Apply Empty_Subq_eq to the current goal.

We will prove SNoR 0 ⊆ Empty.

Let z be given.

Assume Hz: z ∈ SNoR 0.

We prove the intermediate claim Lz: z ∈ SNoS_ 0.

rewrite the current goal using SNoLev_0 (from right to left).

We will prove z ∈ SNoS_ (SNoLev 0).

An exact proof term for the current goal is SNoR_SNoS_ 0 z Hz.

Apply SNoS_E2 0 ordinal_Empty z Lz to the current goal.

Assume Hz1: SNoLev z ∈ 0.

We will prove False.

An exact proof term for the current goal is EmptyE (SNoLev z) Hz1.

∎