Let x and y be given.

Assume Hx Hy.

We will prove ∃x', F x' ∧ ∃y', F y' ∧ pair_tag x y = pair_tag x' y'.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hx.

We use y to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hy.

Use reflexivity.

∎