exists (Finite.get α i)
α✝ : Type ?u.1482
inst : Finite α✝
α : Type u_1
inst✝ : Finite α
p : α → Bool
h✝ : Finite.all p = false
i : Fin toArray.size
h : p (Finite.get α i) = false
⊢ ∃ x, p x = false
no goals