Let q be given.

Assume H1: SNo_ 0 q.

Apply SNoLev_0_eq_0 to the current goal.

An exact proof term for the current goal is SNo_SNo 0 ordinal_Empty q H1.

An exact proof term for the current goal is SNoLev_uniq2 0 ordinal_Empty q H1.

∎