An exact proof term for the current goal is SNoCutP_SNoCut_lim ω omega_ordinal omega_ordsucc.