Let n be given.

Assume Hn.

We will prove n ∈ ω ∪ {- k|k ∈ ω}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hn.

∎