intro h
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
⊢ findP?.loop idx as p = some a → p a = true
α : Type u_1
p : α → Bool
a : α
as : Array α
idx : Nat
h : findP?.loop idx as p = some a
⊢ p a = true