Let x be given.

Assume Hx: SNo x.

Let z be given.

Assume Hz: z ∈ SNoR x.

Let p be given.

Assume Hp.

Apply SepE (SNoS_ (SNoLev x)) (λz ⇒ x < z) z Hz to the current goal.

Assume Hz1: z ∈ SNoS_ (SNoLev x).

Assume Hz2: x < z.

Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) z Hz1 to the current goal.

Assume Hz3: SNoLev z ∈ SNoLev x.

Assume Hz4: ordinal (SNoLev z).

Assume Hz5: SNo z.

Assume Hz6: SNo_ (SNoLev z) z.

An exact proof term for the current goal is Hp Hz5 Hz3 Hz2.

∎