apply Iff.intro
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ∨ x ∈ ys ↔ x ∈ xs ++ ys
case mp
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ∨ x ∈ ys → x ∈ xs ++ ys

case mpr
α : Type u_1
x : α
xs ys : List α
⊢ x ∈ xs ++ ys → x ∈ xs ∨ x ∈ ys