Let x be given.

Assume Hx: SNo x.

Let w be given.

Assume Hw: w ∈ SNoL x.

Let p be given.

Assume Hp.

Apply SepE (SNoS_ (SNoLev x)) (λw ⇒ w < x) w Hw to the current goal.

Assume Hw1: w ∈ SNoS_ (SNoLev x).

Assume Hw2: w < x.

Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) w Hw1 to the current goal.

Assume Hw3: SNoLev w ∈ SNoLev x.

Assume Hw4: ordinal (SNoLev w).

Assume Hw5: SNo w.

Assume Hw6: SNo_ (SNoLev w) w.

An exact proof term for the current goal is Hp Hw5 Hw3 Hw2.

∎