rewrite [List.erase_cons]
case cons
α : 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
⊢ countP p (a' :: l) = countP p (List.erase (a' :: l) a) + 1
case cons
α : 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
⊢ countP p (a' :: l) = countP p (if a' = a then l else a' :: List.erase l a) + 1