Let x be given.

Assume Hx.

Let y be given.

Assume Hy.

We will prove pa x y ∈ complex.

rewrite the current goal using tuple_2_0_eq x y (from right to left).

rewrite the current goal using tuple_2_1_eq x y (from right to left) at position 2.

We will prove pa ((x,y) 0) ((x,y) 1) ∈ complex.

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

We will prove (x,y) ∈ real ⨯ real.

An exact proof term for the current goal is tuple_2_setprod real real x Hx y Hy.

∎