Let X, Tx, Y and V be given.

Assume HV: V ∈ Tx.

We prove the intermediate claim HVsub: V ∩ Y ⊆ Y.

An exact proof term for the current goal is (binintersect_Subq_2 V Y).

We prove the intermediate claim HVpow: V ∩ Y ∈ 𝒫 Y.

An exact proof term for the current goal is (PowerI Y (V ∩ Y) HVsub).

We prove the intermediate claim Hex: ∃V0 ∈ Tx, (V ∩ Y) = V0 ∩ Y.

We use V to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HV.

Use reflexivity.

An exact proof term for the current goal is (SepI (𝒫 Y) (λU0 : set ⇒ ∃V0 ∈ Tx, U0 = V0 ∩ Y) (V ∩ Y) HVpow Hex).

∎