Let alpha be given.

Assume Ha.

Let x be given.

Assume Hx: x ∈ SNoS_ alpha.

Apply SNoS_E2 alpha Ha x Hx to the current goal.

Assume Hx1: SNoLev x ∈ alpha.

Assume Hx2: ordinal (SNoLev x).

Assume Hx3: SNo x.

Assume Hx4: SNo_ (SNoLev x) x.

We prove the intermediate claim Lbmx: SNo_ (SNoLev x) (- x).

An exact proof term for the current goal is minus_SNo_SNo_ (SNoLev x) Hx2 x Hx4.

An exact proof term for the current goal is SNoS_I alpha Ha (- x) (SNoLev x) Hx1 Lbmx.

∎