An exact proof term for the current goal is SNo_SNo (ordsucc (SNoLev x)) (ordinal_ordsucc (SNoLev x) (SNoLev_ordinal x Hx)) (SNo_extend1 x) (SNo_extend1_SNo_ x Hx).