apply Or.intro_left
case mpr.cons.tail.nil
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x (List.append xs [])
⊢ x ∈ z :: xs ∨ x ∈ []
case mpr.cons.tail.nil.h
α : Type u_1
x z : α
xs : List α
ih : x ∈ xs ++ [] → x ∈ xs ∨ x ∈ []
h' : Mem x (List.append xs [])
⊢ x ∈ z :: xs