constructor
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ x ∈ xs ∧ zs ⊆ xs
case left
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ x ∈ xs

case right
α : Type
xs ys zs : List α
x : α
h1 : zs ⊆ xs
h2 : x ∈ ys
h3 : ys ⊆ xs
⊢ zs ⊆ xs