Let x be given.

Assume Hx.

Let w be given.

Assume Hw: w ∈ SNoL x.

Apply SNoL_E x Hx w Hw to the current goal.

Assume Hw1: SNo w.

Assume Hw2: SNoLev w ∈ SNoLev x.

Assume Hw3: w < x.

We will prove w ∈ SNoS_ (SNoLev x).

An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.

∎