apply ih
case cons.nil
α : 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))
⊢ length (foldl (fun acc v => incrCounts acc v) [(x, 1)] xs) = length (uniqueAux xs [x])
no goals