pushing on decs_to_i2_correct

looks like there might be an issue with the semantics of
evaluate_decs_i1; also maybe cenv_inv_to_mod is too weak (should it be
using build_exh_env?).