Assume H0.

Let x be given.

Assume Hx.

We will prove ∃x', F x' ∧ ∃y, F y ∧ x = 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 0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H0.

Use symmetry.

An exact proof term for the current goal is pair_tag_0 x.

∎