simp [uniqueAux]
case nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
as cs : List α
⊢ length (uniqueAux [] (cs ++ x :: (as ++ [y]))) = length (uniqueAux [] (cs ++ y :: x :: as))
case nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
as cs : List α
⊢ Nat.succ (length as + Nat.succ 0 + length cs) = length as + Nat.succ 0 + Nat.succ 0 + length cs