Started work on making exhLang have a value relation

The correctness proof into exhLang needs to use a value relation,
instead of a function on values. With a function, the proof can only
talk about the compilers current type to constructor mapping, which
makes it very hard to use the theorem to reason about the compiler for
building a REPL because the constructor mapping will be updated, and you
still need to know about the old values.

To fix the problem, values will be related if there is a submap of the
constructor mapping under which the translation from decLang to exhLang
gives the right answer. This builds the right weakening property into
the value relation, and is how things were handled in modLang and
conLang.
State the correctness theorem
Fix the statement.
Merge branch 'cenv_close' into exhLang_value_rel
comment out unfinished proof
get free_varsScript.sml working with new v_to_exh
start on making compiler proofs use new v_to_exh relation

looks promising, but haven't covered the hard parts yet
prove all the exh-related cheats in compile_top_thm

but added a cheat for v_to_exh_extend_disjoint to do so
move v_to_exh_extend_disjoint to exhLangProofScript.sml
bit of work on new exp_to_exh_correct
Prove v_to_exh_extend_disjoint
Merge remote-tracking branch 'origin/cenv_close' into exhLang_value_rel