Let n be given.

Assume Hn.

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

Apply binunionI2 to the current goal.

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

Apply ReplI to the current goal.

An exact proof term for the current goal is Hn.

∎