Let x1, y1, x2 and y2 be given.

Assume Heq.

Apply andI to the current goal.

We will prove x1 = x2.

rewrite the current goal using (R2_xcoord_tuple x1 y1) (from right to left).

rewrite the current goal using (R2_xcoord_tuple x2 y2) (from right to left).

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

Use reflexivity.

We will prove y1 = y2.

rewrite the current goal using (R2_ycoord_tuple x1 y1) (from right to left).

rewrite the current goal using (R2_ycoord_tuple x2 y2) (from right to left).

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

Use reflexivity.

∎