Let x be given.

Assume Hx: SNo x.

Set alpha to be the term SNoLev x.

We prove the intermediate claim La: ordinal alpha.

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 alpha) (ordinal_ordsucc alpha La) (λdelta ⇒ delta ∈ x ∨ delta = alpha).

∎