Let x1, y1, x2 and y2 be given.

Assume Hx: x1 = x2.

Assume Hy: y1 = y2.

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

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

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

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

Use reflexivity.

∎