simp only [htrue, ite_true, incrCounts, map]
case cons.cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ length
      (foldl (fun acc v => incrCounts acc v)
        (if a.fst = x then (a.fst, a.snd + 1) :: as else (a.fst, a.snd) :: incrCounts as x) xs) =
    length
      (if x ∈ map Prod.fst (a :: as) then uniqueAux xs (map Prod.fst (a :: as))
      else uniqueAux xs (x :: map Prod.fst (a :: as)))
case cons.cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih :
  ∀ (acc : List (α × Nat)),
    length (foldl (fun acc v => incrCounts acc v) acc xs) = length (uniqueAux xs (map Prod.fst acc))
a : α × Nat
as : List (α × Nat)
htrue : a.fst = x
⊢ length (foldl (fun acc v => incrCounts acc v) ((x, a.snd + 1) :: as) xs) =
    length
      (if x ∈ x :: map Prod.fst as then uniqueAux xs (x :: map Prod.fst as)
      else uniqueAux xs (x :: x :: map Prod.fst as))