. 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 _
case mp
α : 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 α
⊢ z ∈ cs ++ x :: (as ++ [y]) → z ∈ cs ++ y :: x :: as

case mpr
α : 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 α
⊢ z ∈ cs ++ y :: x :: as → z ∈ cs ++ x :: (as ++ [y])
case mpr
α : 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 α
⊢ z ∈ cs ++ y :: x :: as → z ∈ cs ++ x :: (as ++ [y])