Let X be given.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ intersection_of_family X Empty.
We will prove x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U : set, U ∈ Empty → x0 ∈ U) x Hx).
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ intersection_of_family X Empty.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ ∀U : set, U ∈ Empty → x0 ∈ U) x HxX (λU HU ⇒ EmptyE U HU (x ∈ U))).
∎