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

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).