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