prove compile_decs_wrap_divergence

again with a lot of copying from compile_decs_wrap_thm
prove compile_top_divergence

(also, minor fixes so compiler/proofs builds)

This completes compilerProofsTheory with the exception of one cheat for
a lemma: env_rs_shift_menv, saying that the invariant is maintaned when
the top of the environment is shifted into the module environment.