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