cases Classical.em (a == x) with
| inl hx =>
  rw [List.count, List.countp, List.countp.go, List.countp.go_accum]
  simp [hx]
  ac_rfl
| inr hx =>
  rw [List.count, List.countp, List.countp.go, List.countp]
  simp [hx]
α : Type
inst✝ : BEq α
x a : α
as : List α
⊢ List.count x (a :: as) = (bif a == x then 1 else 0) + List.count x as
no goals