simp only [uniqueAux, foldl]
case cons
α : 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))
acc : List (α × Nat)
⊢ length (foldl (fun acc v => incrCounts acc v) acc (x :: xs)) = length (uniqueAux (x :: xs) (map Prod.fst acc))
case cons
α : 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))
acc : List (α × Nat)
⊢ length (foldl (fun acc v => incrCounts acc v) (incrCounts acc x) xs) =
    length (if x ∈ map Prod.fst acc then uniqueAux xs (map Prod.fst acc) else uniqueAux xs (x :: map Prod.fst acc))