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