simp only [if_true, countP_cons, hp, if_neg, Nat.add_zero]
case refl
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = false
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a)
ha : a ∈ a :: l
⊢ countP p (a :: l) = countP p (if a = a then l else a :: List.erase l a)
no goals