Let p be given.

Assume Hp.

We will prove (R2_xcoord p,R2_ycoord p) = p.

Apply (Sigma_E R (λ_ : set ⇒ R) p Hp) to the current goal.

Let x be given.

Assume Hx_pair.

Apply Hx_pair to the current goal.

Assume HxR Hexy.

Apply Hexy to the current goal.

Let y be given.

Assume Hy_pair.

Apply Hy_pair to the current goal.

Assume HyR Hpeq.

We prove the intermediate claim HeqT: p = (x,y).

We will prove p = (x,y).

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

An exact proof term for the current goal is Hpeq.

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

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

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

Use reflexivity.

∎