Let x1, y1, x2 and y2 be given.

Assume Hx1 Hy1 Hx2 Hy2.

Assume H1: pair_tag x1 y1 = pair_tag x2 y2.

Apply set_ext to the current goal.

An exact proof term for the current goal is pair_tag_prop_2_Subq x1 y1 x2 y2 Hy1 Hx2 Hy2 H1.

Apply pair_tag_prop_2_Subq x2 y2 x1 y1 Hy2 Hx1 Hy1 to the current goal.

Use symmetry.

An exact proof term for the current goal is H1.

∎