apply decide_eq_true
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
⊢ decide (∀ (x : α), p x) = true
case a
α : Type u_1
inst : Finite α
p : α → Prop
inst✝ : DecidablePred p
h : (Finite.all fun x => decide (p x)) = true
⊢ ∀ (x : α), p x