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