α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
⊢ (count a l + if a = b then 1 else 0) = if a = b then succ (count a l) else count a l
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
⊢ count a (b :: l) = if a = b then succ (count a l) else count a l
simp [count_cons']
no goals
α : Type u_1
l✝ : List α
inst✝ : DecidableEq α
a b : α
l : List α
⊢ (count a l + if a = b then 1 else 0) = if a = b then succ (count a l) else count a l
split_ifs <;> rfl