work towards getting exp_to_Cexp_thm1 building again
more exp_to_Cexp_thm1

will need to modify the definition, though, so that it calls exp_to_Cexp
with the correct bvars at all times (currently it uses a call under a
let because it knows what the environment is, but it's easier for the
proof to ignore that knowledge)
fix bug in exp_to_Cexp_def and work on exp_to_Cexp_thm1

the note last commit about not adding to the bvars merely being for
convenience was wrong: it is necessary for correctness to shift the
variables when introducing a let.