An exact proof term for the current goal is (SepE2 (𝒫 Y) (λU0 : set ⇒ ∃V ∈ Tx, U0 = V ∩ Y) U HU).