no goals
α : Type u_1
β : Type ?u.295572
γ : Type ?u.295575
p : α → Prop
inst✝ : DecidablePred p
b : α
s : Multiset α
⊢ ∀ (a : List α), countp p (b ::ₘ Quot.mk Setoid.r a) = countp p (Quot.mk Setoid.r a) + if p b then 1 else 0
simp [List.countp_cons]