apply Nat.le_trans
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length (uniqueAux xs as) ≤ length xs + 1 + length as
case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ length (uniqueAux xs as) ≤ ?cons.inl.m

case cons.inl.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ ?cons.inl.m ≤ length xs + 1 + length as

case cons.inl.m
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
as : List α
h : x ∈ as
⊢ Nat