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