work on letrec case, make good_code_env_def stronger

this suggests that label_closures_thm needs to be slightly stronger, so
might want to check that what is desired can be proven first...
thoughts about extended statement for label_closures_thm
prove extended label_closures_thm
add another condition to good_code_env, and update label_closures_thm
prove first half of function calls in compile_val

cheating in function creation, because wanted to skip forward to
function calls to see if that works... now might be good to go back,
since this was unexpected given the simplifications made to Cv_bv.
remove some cheats in letrec case

three cheats remain
remove cheats from letrec, two in fun remain
prove all cheats in closure creation

now just need to do check the second half of function calls works. the
rest after that will likely go through with tedious but easy updates.
finish function call case
finish proving rest of compile_val
Merge branch 'deBruijn'

The compiler proofs now build in the old language without modules. The
intermediate language now uses deBruijn indices.

The proofs won't work here on master, since the source language has
modules; my next task is to upgrade the compiler to handle them.
Possibly after proving a connect-everything-up theorem:

The theorems so far proved are not quite complete, because there is no
top-level theorem putting together all the pieces of the compiler, and
hence there are some pieces of compile_Cexp about which I still haven't
proved anything. But I think the missing pieces are all fairly trivial.
Then again, it was the last attempt to do the top-level theorem that
prompted the long trek to the land of deBruijn indices.