added evaluator in Env (used in Env.rewrite);
Env.rewrite used in basic_simplify, making rewrite rules
more pervasively used
bugfixes in modularArith; also use Arith.T term constructors
simplifying arithmetic term constructors in Arith.T
ArithElim: big chunk of modular arithmetic implemented,
with term/literal rewrite rules for simplifications, enumeration of divisors, enumeration of cases for modulo