work on env_rs_shift_to_menv
more work on shift_to_menv, and a paragraph on why it should be true

this will have to merge onto the master branch at some point, but I
don't want to ruin anyone's build..
prove another piece of shift_to_menv
more work towards shift_to_menv

as part of this, proved syneq_sym_all_vlabs, to complement
syneq_sym_no_vlabs, and show that syneq really is symmetric on the two
ILs.

move various needed lemmas around to get everything else to keep building.
Merge branch 'master' into shift_to_menv

Conflicts:
	compiler/proofs/compilerProofsScript.sml
(because the hand proof had been copied across)
make replCorrect build again

had to introduce a cheat about the type system ensuring that all module
names are distinct (I guess that should be easy to prove but not by me)
reduce env_rs_shift_to_menv to one cheat

pick a better witness for the new module environment - makes everything
much easier.

the remaining subgoal is about code_env_cd still holding, which I think
might require proving that the compiler generates the same code if
called with an extended module environment.
prove compiler generates same code if menv is extended

as long as the mvars appearing in the expression were already all bound.

had to define mvars - apparently before was just relying on the
semantics to never look up unbound variables. also, add this closed
condition to the definition of code_env_cd, and update the compile_val
proof. the other proof that will likely be affected is the correctness
of compile_code_env (not yet updated).
WIP on pushing the mvars stuff up through everything else
finish proof of mvars_exp_to_Cexp
get compiler tests building again
couple of test attempting to break module variable lookup

but it seems to work, so will try again to prove it...
prove env_rs_shift_to_menv

change the code_env_cd condition on the rmenv: the variable is an index
into the environment, so needs to be less than its length (rather than a
member of it). with this change, things go through easier.
Merge branch 'master' into shift_to_menv

checking that everything builds now that the cheat is gone from
compilerProofsScript.sml
comment out broken proof in interactiveScript.sml
fix PrintE_thm for slight changes to bc_eval

The only cheats in replCorrect now are:
  - want to get all module names distinct from type system
  - repl_fun_alt/prime version of the replCorrect lemma