exact Or.intro_right _ hxys
case mpr.cons.tail.cons.inr
α : Type u_1
x z : α
xs : List α
y : α
ys : List α
ih : x ∈ xs ++ y :: ys → x ∈ xs ∨ x ∈ y :: ys
h' : Mem x (xs ++ y :: ys)
hxys : x ∈ y :: ys
⊢ x ∈ z :: xs ∨ x ∈ y :: ys
no goals