no goals
case h.e'_3.h.e'_6
α : Type u_1
β : Type ?u.313067
γ : Type ?u.313070
p✝ : α → Prop
inst✝² : DecidablePred p✝
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
l : List α
⊢ countp p (filter (fun a => ¬q a) (Quot.mk Setoid.r l)) =
    List.countp (fun x => decide (p x)) (List.filter (fun a => decide ¬decide (q a) = true) l)
simp