An exact proof term for the current goal is SNoS_I (SNoLev y) (SNoLev_ordinal y Hy) x (SNoLev x) Hxy (SNoLev_ x Hx).