An exact proof term for the current goal is SNoLev_uniq2 (ordsucc (SNoLev x)) (ordinal_ordsucc (SNoLev x) (SNoLev_ordinal x Hx)) (SNo_extend0 x) (SNo_extend0_SNo_ x Hx).