no goals
α : Type u_1
β : Type ?u.438273
γ : Type ?u.438276
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_and_right, exists_or, exists_eq_left]