relax type constraint on cenv in proofs

there may be some inconsistency in the semantics as to where envC is
wanted versus an environment with a different range type... for now just
make my proofs as general as possible.
found the source of type inconsistency

I had manually instantiated the type variable in evaluate_strongind, to
make it match envC. Since the latter has now changed, this
instantiation has to change too.
update toIntLangProofs for new exceptions
remove reference to CompilerPrimitivesTheory from toBytecodeProofs

the latter then builds unchanged