Let U, V, x and y be given.

Assume Hx: x ∈ U.

Assume Hy: y ∈ V.

We will prove (x,y) ∈ rectangle_set U V.

rewrite the current goal using rectangle_set_def (from left to right).

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 U (λ_ : set ⇒ V) x Hx y Hy).

∎