theorem List.findIdx?_eq_some_le_of_findIdx?_eq_some {α : Type u_1} {xs : List α} {p : α → Bool} {q : α → Bool} (w : ∀ (x : α), x ∈ xs → p x = true → q x = true) {i : Nat} (h : List.findIdx? p xs = some i) : ∃ (j : Nat), j ≤ i ∧ List.findIdx? q xs = some j