Let X, Y, x and y be given.

Assume Hx: x ∈ X.

Assume Hy: y ∈ Y.

We will prove (x,y) ∈ setprod X Y.

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

An exact proof term for the current goal is (pair_Sigma X (λ_ : set ⇒ Y) x Hx y Hy).

∎