Let z be given.
Assume Hz: SNo z.
Apply SNoLev_prop z Hz to the current goal.
Assume Hz1: ordinal (SNoLev z).
Assume Hz2: SNo_ (SNoLev z) z.
An exact proof term for the current goal is SNoS_I (ordsucc (SNoLev z)) (ordinal_ordsucc (SNoLev z) Hz1) z (SNoLev z) (ordsuccI2 (SNoLev z)) Hz2.
∎