simp [hp, ih]
case cons.inr
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
hp : ¬p a = true
⊢ (bif p a then List.countp.go p as' (acc + 1) else List.countp.go p as' acc) =
    (bif p a then List.countp.go p as' 1 else List.countp.go p as' 0) + acc
no goals