absurd forall_eq_false_of_any_eq_false h x
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ False
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.any fun x => decide (p x)) = false
x : α
hx : p x
⊢ ¬decide (p x) = false