no goals
α : Type u_1
β : Type ?u.336299
γ : Type ?u.336302
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
_l : List α
⊢ countp p (Quot.mk Setoid.r _l) = 0 ↔ ∀ (a : α), a ∈ Quot.mk Setoid.r _l → ¬p a
simp