intros as
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
⊢ ∀ (as : List α), length (uniqueAux (x :: xs) as) ≤ length (x :: xs) + length as
case cons
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
⊢ length (uniqueAux (x :: xs) as) ≤ length (x :: xs) + length as