Let x be given.

Assume Hx: SNo x.

Set alpha to be the term SNoLev x.

We prove the intermediate claim La: ordinal α.

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

An exact proof term for the current goal is SNo_PSNo (ordsucc α) (ordinal_ordsucc α La) (λδ ⇒ δ ∈ x ∨ δ = α).

∎