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_Pi_closed U HUT HU X HX (λ_ ⇒ Y) (λx Hx ⇒ HY).

∎