simp only [all]
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ (all xs fun x => decide (p x)) = true ↔ ∀ (x : α), x ∈ xs → p x
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
xs : List α
⊢ foldr (fun a r => decide (p a) && r) true xs = true ↔ ∀ (x : α), x ∈ xs → p x