Let x be given.

Assume Hx.

Let z be given.

Assume Hz: z ∈ SNoR x.

Apply SNoR_E x Hx z Hz to the current goal.

Assume Hz1: SNo z.

Assume Hz2: SNoLev z ∈ SNoLev x.

Assume Hz3: x < z.

We will prove z ∈ SNoS_ (SNoLev x).

An exact proof term for the current goal is SNoS_I2 z x Hz1 Hx Hz2.

∎