ac_rfl
case cons.inl
α : Type
p : α → Bool
a : α
as' : List α
ih : ∀ (acc : ℕ), List.countp.go p as' acc = List.countp p as' + acc
acc : ℕ
hp : p a = true
⊢ List.countp p as' + (acc + 1) = List.countp p as' + 1 + acc
no goals