induction as generalizing acc with
| nil           => simp [List.countp.go, List.countp]
| cons a as' ih =>
  simp [List.countp, List.countp.go]
  cases Classical.em (p a) with
  | inl hp =>
    simp [hp, ih]
    ac_rfl
  | inr hp => simp [hp, ih]
α : Type
p : α → Bool
as : List α
acc : ℕ
⊢ List.countp.go p as acc = List.countp p as + acc
no goals