Let x1, y1, x2 and y2 be given.
Assume Heq.
Apply andI to the current goal.
We will prove x1 = x2.
We prove the intermediate claim Hproj0: (x1,y1) 0 = (x2,y2) 0.
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hx1: (x1,y1) 0 = x1.
An exact proof term for the current goal is (tuple_2_0_eq x1 y1).
We prove the intermediate claim Hx2: (x2,y2) 0 = x2.
An exact proof term for the current goal is (tuple_2_0_eq x2 y2).
rewrite the current goal using Hx1 (from right to left).
rewrite the current goal using Hx2 (from right to left).
An exact proof term for the current goal is Hproj0.
We will prove y1 = y2.
We prove the intermediate claim Hproj1: (x1,y1) 1 = (x2,y2) 1.
rewrite the current goal using Heq (from left to right).
Use reflexivity.
We prove the intermediate claim Hy1: (x1,y1) 1 = y1.
An exact proof term for the current goal is (tuple_2_1_eq x1 y1).
We prove the intermediate claim Hy2: (x2,y2) 1 = y2.
An exact proof term for the current goal is (tuple_2_1_eq x2 y2).
rewrite the current goal using Hy1 (from right to left).
rewrite the current goal using Hy2 (from right to left).
An exact proof term for the current goal is Hproj1.
∎