α : Type u_1
l : List α
inst✝ : DecidableEq α
a : α
⊢ (if a = a then succ (count a []) else count a []) = 1
α : Type u_1
l : List α
inst✝ : DecidableEq α
a : α
⊢ count a [a] = 1
rw [count_cons]
no goals
α : Type u_1
l : List α
inst✝ : DecidableEq α
a : α
⊢ (if a = a then succ (count a []) else count a []) = 1
simp