Let x be given.
Assume Hx.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
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.