Let p be given.
Assume Hp1 Hp2.
Let x be given.
Assume Hx.
We will prove p x.
Apply binunionE ω {- n|n ∈ ω} x Hx to the current goal.
Assume Hx: x ∈ ω.
An exact proof term for the current goal is Hp1 x Hx.
Assume Hx.
Apply ReplE_impred ω minus_SNo x Hx to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hxn: x = - n.
rewrite the current goal using Hxn (from left to right).
An exact proof term for the current goal is Hp2 n Hn.
∎