work on compile_top_thm, and look at case where module fails

and we add the module name with an empty environment to the rmenv. but
verifying env_rs after that addition looks hard - and I want to make
sure it's necessary first, so will rid of it in next commit. after all, the
implementation only needs the rmenv to look stuff up that it will
actually find... i.e. empty envs are useless..
remove rmenv |+ (mn,[]) from the compiler

that indeed makes that case go through easily.
however, there is still the case where we have to add a real module
environment, and that is probably going to be harder than I thought. At
least, I probably have to prove that the compiler produces the same code
if you give it an extended module environment... or maybe change
code_env_cd (and whatever calls it) to not treat the menv as fixed but
take it in as a parameter..
Prove compile_print_dec_thm

This leaves one cheat in compilerProofs (for shifting an environment
into the module environment).

After that (or maybe I'll do them before), the theorems about divergence
still need to be proved, then this theory will finally be finished.