apply Or.intro_left
case mpr.cons.tail.cons.inl
α : 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)
hxxs : x ∈ xs
⊢ x ∈ z :: xs ∨ x ∈ y :: ys
case mpr.cons.tail.cons.inl.h
α : 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)
hxxs : x ∈ xs
⊢ x ∈ z :: xs