An exact proof term for the current goal is SNoS_omega_real 1 (omega_SNoS_omega 1 (nat_p_omega 1 nat_1)).