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 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 α
h : z ∈ cs ++ y :: x :: as
⊢ z ∈ cs ++ x :: (as ++ [y])
no goals