reduce the cheat in compile_top_thm to a need for env_rs_shift_to_menv

isolates the difficulty in a somewhat plausible looking conjecture
first half of compile_decs_divergence

easy case, where the divergence happens on the first tried declaration.
next case should follow from the inductive hypothesis, though, just need
to push the invariants across...
bit of progress on compile_decs_divergence
start on compile_call_val theorem

This theorem is for relating an intermediate language CCall of a
variable bound to a closure on variables bound to arguments that results
in a value, to an execution of bytecode in an appropiate starting state
to yield a refinement of the value. haven't completely figured out
"appropriate starting state" yet.

Likely going to use the Cenv_bs_bind_fv theorem to say the required
environment for evaluating the body can be created by using the values
inside the bytecode closure environment