exact IH <| (mem_cons.mp ha).resolve_left (Ne.symm h)
α : Type u
β : Type v
inst✝ : DecidableEq α
p : α → Bool
a : α
hp : p a = true
a' : α
l : List α
IH : a ∈ l → countP p l = countP p (List.erase l a) + 1
ha : a ∈ a' :: l
h : ¬a' = a
⊢ countP p l = countP p (List.erase l a) + 1
no goals