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