apply Iff.intro
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ y :: ys ↔ x ∈ [y] ∨ x ∈ ys
case mp
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ y :: ys → x ∈ [y] ∨ x ∈ ys

case mpr
α : Type u_1
y : α
ys : List α
x : α
⊢ x ∈ [y] ∨ x ∈ ys → x ∈ y :: ys