simp only [find?, Quotient.lift_mk, List.find?_eq_none, Bool.not_eq_true]
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
L : List α
⊢ find? f ⟦L⟧ h = none ↔ ∀ x ∈ ⟦L⟧, f x = false
case refl
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
L : List α
⊢ (∀ x ∈ L, f x = false) ↔ ∀ x ∈ ⟦L⟧, f x = false