constructor
case a
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
⊢ x ∈ Set.empty.inter s ↔ x ∈ Set.empty
case a.mp
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
⊢ x ∈ Set.empty.inter s → x ∈ Set.empty

case a.mpr
α : Sort u_1
β : ?m.13358
γ : ?m.13361
s : Set α
x : α
⊢ x ∈ Set.empty → x ∈ Set.empty.inter s