Let z be given.

Assume Hz.

Let y be given.

Assume Hy Hyz Hzy.

We will prove y ∈ SNoR z.

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

Apply SepI to the current goal.

We will prove y ∈ SNoS_ (SNoLev z).

An exact proof term for the current goal is SNoS_I2 y z Hy Hz Hyz.

We will prove z < y.

An exact proof term for the current goal is Hzy.

∎