no goals
α : Type u_1
β : Type ?u.37873
γ : Type ?u.37876
s t : Finset α
a b : α
h : ¬a ∈ s
p : α → Prop
⊢ (∀ (x : α), x ∈ cons a s h → p x) ↔ p a ∧ ∀ (x : α), x ∈ s → p x
simp only [mem_cons, or_imp, forall_and, forall_eq]