no goals
α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidableEq α
x y : α
⊢ ↑(count x) (of y) = Pi.single x 1 y
simp [Pi.single, Function.update, count, countp, List.countp, List.countp.go,
  Bool.beq_eq_decide_eq]