no goals
α : Type u_1
β : Type ?u.438931
γ : Type ?u.438934
inst✝ : DecidableEq α
a : α
s : Finset α
p : α → Prop
⊢ (∀ (x : α), x ∈ insert a s → p x) ↔ p a ∧ ∀ (x : α), x ∈ s → p x
simp only [mem_insert, or_imp, forall_and, forall_eq]