Let z be given.

Assume Hz.

Let p be given.

Assume Hp.

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

Let u be given.

Assume Hu: u ∈ complex ⨯ complex.

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

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

∎