apply h <;> assumption
case refl.mpr.intro.tail.h_1
α : Type u_1
f : α → Bool
h : ∀ (a1 a2 : α), f a1 = true → f a2 = true → a1 = a2
x : α
L : List α
h2 : f x = true
b✝ : α
as✝ : List α
a✝ : List.Mem x as✝
a_ih✝ : List.find? f as✝ = some x
x✝ : Bool
heq✝ : f b✝ = true
⊢ b✝ = x
no goals