Lemmas about List.find?

theorem List.find?_eq_find?_of_perm {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α} (h : l₁.Perm l₂) (hp : {x : α | x ∈ l₁ ∧ p x = true}.Subsingleton) : find? p l₁ = find? p l₂

If there is at most one element satisfying p, then find? agrees on permuted lists.

theorem List.find?_congr {α : Type u_1} {p₁ p₂ : α → Bool} {l : List α} (h : ∀ (x : α), x ∈ l → p₁ x = p₂ x) : find? p₁ l = find? p₂ l

If two predicates agree on all the elements, so does find?.