Let x be given.

Assume Hx.

Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.

Assume Hx1: SNoLev x ∈ ω.

Assume Hx2: ordinal (SNoLev x).

Assume Hx3: SNo x.

Assume Hx4: SNo_ (SNoLev x) x.

Apply SNoS_I ω omega_ordinal (- x) (SNoLev (- x)) to the current goal.

We will prove SNoLev (- x) ∈ ω.

rewrite the current goal using minus_SNo_Lev x Hx3 (from left to right).

We will prove SNoLev x ∈ ω.

An exact proof term for the current goal is Hx1.

We will prove SNo_ (SNoLev (- x)) (- x).

Apply SNoLev_ to the current goal.

An exact proof term for the current goal is SNo_minus_SNo x Hx3.

∎