constructor
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ s.inter t
case left
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ s

case right
α : Sort u_1
s t u : Set α
hus : u.Subset s
hut : u.Subset t
x : α
hxu : x ∈ u
⊢ x ∈ t