Let x1, y1, x2 and y2 be given.

Assume Hx1 Hx2.

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_1_Subq x1 y1 x2 y2 Hx1 H1.

Apply pair_tag_prop_1_Subq x2 y2 x1 y1 Hx2 to the current goal.

Use symmetry.

An exact proof term for the current goal is H1.

∎