cases Decidable.em (x ∈ as) with
| inl h =>
  simp only [length, uniqueAux, h, ite_true]
  apply Nat.le_trans
  apply ih
  rw [Nat.add_assoc, Nat.add_comm 1, ←Nat.add_assoc]
  apply Nat.le_step
  simp
| inr h =>
  simp only [length, uniqueAux, h, ite_false]
  apply Nat.le_trans
  apply ih
  simp only [length]
  rw [Nat.add_comm _ 1, Nat.add_assoc]
  apply Nat.le_refl
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
no goals