no goals
α : Type u_1
β : Type ?u.127828
γ : Type ?u.127831
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ Finset.subtype p s = ∅ ↔ ∀ (x : α), p x → ¬x ∈ s
simp [ext_iff, Subtype.forall, Subtype.coe_mk]