rw [uniqueAux_acc_append _ _ h, length_append, length_reverse, Nat.add_comm]
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
⊢ length (uniqueAux xs acc) = length (unique xs) + length acc
no goals