An exact proof term for the current goal is SNoS_omega_real 0 (omega_SNoS_omega 0 (nat_p_omega 0 nat_0)).