Let z be given.

Assume Hz.

Let x be given.

Assume Hx Hxz1 Hxz2.

We will prove x ∈ SNoL z.

We will prove x ∈ {x ∈ SNoS_ (SNoLev z)|x < z}.

Apply SepI to the current goal.

We will prove x ∈ SNoS_ (SNoLev z).

An exact proof term for the current goal is SNoS_I2 x z Hx Hz Hxz1.

We will prove x < z.

An exact proof term for the current goal is Hxz2.

∎