simp only [map, incrCounts]
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
⊢ map Prod.fst (incrCounts (a :: as) x) = map Prod.fst (a :: as) ++ [x]
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
a : α × Nat
as : List (α × Nat)
ih : ¬x ∈ map Prod.fst as → map Prod.fst (incrCounts as x) = map Prod.fst as ++ [x]
h : ¬x ∈ map Prod.fst (a :: as)
⊢ map Prod.fst (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) =
    a.fst :: map Prod.fst as ++ [x]