Let z be given.

Assume Hz.

Apply Eps_i_ex (λx ⇒ F x ∧ ∃y, F y ∧ z = pa x y) to the current goal.

We will prove ∃x, F x ∧ ∃y, F y ∧ z = pa x y.

An exact proof term for the current goal is Hz.

∎