match exists_eq_false_of_all_eq_false h with
| ⟨x, hx⟩ =>
  intro h
  rw [decide_eq_true (h x)] at hx
  contradiction
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = false
⊢ ¬∀ (x : α), p x
no goals