Let U be given.

Assume HUT HU.

Let X be given.

Assume HX.

Let Y be given.

Assume HY.

An exact proof term for the current goal is ZF_Sigma_closed U HUT HU X HX (λ_ ⇒ Y) (λ_ _ ⇒ HY).

∎