rw [←cons_append] at hcons
case mp.inr.a
α : 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 ++ x :: (as ++ [y])
hcons : z ∈ x :: (as ++ [y])
⊢ z ∈ y :: x :: as
case mp.inr.a
α : 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 ++ x :: (as ++ [y])
hcons : z ∈ x :: as ++ [y]
⊢ z ∈ y :: x :: as