rw [decide_eq_true hx]
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
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
⊢ ¬true = false