Let z be given.

Assume Hz.

Let p be given.

Assume Hp.

Apply ReplE_impred (real ⨯ real) (λu ⇒ pa (u 0) (u 1)) z Hz to the current goal.

Let u be given.

Assume Hu: u ∈ real ⨯ real.

Assume Hzu: z = pa (u 0) (u 1).

An exact proof term for the current goal is Hp (u 0) (ap0_Sigma real (λ_ ⇒ real) u Hu) (u 1) (ap1_Sigma real (λ_ ⇒ real) u Hu) Hzu.

∎