Let x and y be given.

Assume Hx: x ∈ R.

Assume Hy: y ∈ R.

We prove the intermediate claim Hxy: (x,y) ∈ setprod R R.

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma R R x y Hx Hy).

rewrite the current goal using (apply_fun_graph (setprod R R) (λp : set ⇒ R_bounded_distance (p 0) (p 1)) (x,y) Hxy) (from left to right).

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

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

Use reflexivity.

∎