Let α be given.

Assume Ha: ordinal α.

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

Assume H1: ordinal (SNoLev α).

Assume H2: SNo_ (SNoLev α) α.

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

∎