Let U be given.

Assume HU: U ∈ Intersection_Fam X Fam.

An exact proof term for the current goal is (SepE1 (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) U HU).

Let U be given.

Assume HU: U ∈ 𝒫 X.

We prove the intermediate claim HAllT: ∀T : set, T ∈ Fam → U ∈ T.

Let T be given.

Assume HT: T ∈ Fam.

Apply FalseE to the current goal.

Apply HFamEmpty to the current goal.

We use T to witness the existential quantifier.

An exact proof term for the current goal is HT.

An exact proof term for the current goal is (SepI (𝒫 X) (λU0 ⇒ ∀T : set, T ∈ Fam → U0 ∈ T) U HU HAllT).