no goals
α : Type u_1
β : Type ?u.302041
γ : Type ?u.302044
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ ↑card (Quot.mk Setoid.r l) = countp p (Quot.mk Setoid.r l) + countp (fun x => ¬p x) (Quot.mk Setoid.r l)
simp [l.length_eq_countp_add_countp p]