Let α be given.

Assume Ha: ordinal α.

We prove the intermediate claim La1: SNo α.

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

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

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

Apply Empty_Subq_eq to the current goal.

Let x be given.

Assume Hx: x ∈ SNoR α.

Apply SNoR_E α 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 ∈ α.

Assume Hx3: α < x.

We will prove False.

Apply SNoLt_irref x to the current goal.

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

We will prove x < α.

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

We will prove α < x.

An exact proof term for the current goal is Hx3.

∎