Let a, b, c and d be given.

Assume Heq: (a,b) = (c,d).

We will prove a = c.

rewrite the current goal using (tuple_2_0_eq a b) (from right to left) at position 1.

rewrite the current goal using (tuple_2_0_eq c d) (from right to left).

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

Use reflexivity.

∎