Let x be given.

Assume H.

Apply EmptyAx to the current goal.

We use x to witness the existential quantifier.

An exact proof term for the current goal is H.

∎