Let alpha be given.

Assume Ha: ordinal alpha.

Apply SNoLev_prop alpha (ordinal_SNo alpha Ha) to the current goal.

Assume H1: ordinal (SNoLev alpha).

Assume H2: SNo_ (SNoLev alpha) alpha.

An exact proof term for the current goal is SNoLev_uniq alpha (SNoLev alpha) alpha H1 Ha H2 (ordinal_SNo_ alpha Ha).

∎