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