Let x be given.

Assume Hx: SNo x.

Assume H2: ∀y ∈ SNoS_ (SNoLev x), y < x.

We will prove ordinal x.

rewrite the current goal using SNo_max_SNoLev x Hx H2 (from right to left).

We will prove ordinal (SNoLev x).

An exact proof term for the current goal is SNoLev_ordinal x Hx.

∎