have rearrange_mem :
  (z ∈ cs ++ x :: (as ++ [y])) ↔ (z ∈ cs ++ y :: x :: as) := by
  apply Iff.intro
  . intros h
    cases mem_append_iff.mpr h with
    | inl hcs => exact List.mem_append_front _ _ _ hcs
    | inr hcons =>
      apply List.mem_append_back
      rw [←cons_append] at hcons
      cases mem_append_iff.mpr hcons with
      | inl hxas => exact List.Mem.tail _ hxas
      | inr hy =>
        cases hy with
        | tail _ _ => contradiction
        | head _ => exact List.Mem.head _
  . intros h
    cases mem_append_iff.mpr h with
    | inl hcs => exact List.mem_append_front _ _ _ hcs
    | inr hcons =>
      apply List.mem_append_back
      cases hcons with
      | head _ =>
        apply List.Mem.tail
        apply List.mem_append_back
        apply (List.mem_singleton_iff y y).mpr rfl
      | tail _ hcons' =>
        rw [←cons_append]
        exact List.mem_append_front _ _ _ hcons'
case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
⊢ length (uniqueAux (z :: zs) (cs ++ x :: (as ++ [y]))) = length (uniqueAux (z :: zs) (cs ++ y :: x :: as))
case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
⊢ length (uniqueAux (z :: zs) (cs ++ x :: (as ++ [y]))) = length (uniqueAux (z :: zs) (cs ++ y :: x :: as))