induction xs with
| nil => simp [uniqueAux]
| cons x xs ih =>
  intros as
  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
α : Type u_1
inst✝ : DecidableEq α
xs : List α
⊢ ∀ (as : List α), length (uniqueAux xs as) ≤ length xs + length as
no goals