Let alpha be given.

Assume Ha: ordinal alpha.

We prove the intermediate claim La1: SNo alpha.

An exact proof term for the current goal is ordinal_SNo alpha Ha.

We prove the intermediate claim La2: SNoLev alpha = alpha.

An exact proof term for the current goal is ordinal_SNoLev alpha Ha.

Apply Empty_Subq_eq to the current goal.

Let x be given.

Assume Hx: x ∈ SNoR alpha.

Apply SNoR_E alpha La1 x Hx to the current goal.

Assume Hx1: SNo x.

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

Assume Hx2: SNoLev x ∈ alpha.

Assume Hx3: alpha < x.

We will prove False.

Apply SNoLt_irref x to the current goal.

Apply SNoLt_tra x alpha x Hx1 La1 Hx1 to the current goal.

We will prove x < alpha.

An exact proof term for the current goal is ordinal_SNoLev_max alpha Ha x Hx1 Hx2.

We will prove alpha < x.

An exact proof term for the current goal is Hx3.

∎