start work on correctness of compilation of CFun

This commit just adds Fun to the language subset considered.
Unexpectedly, compile_val breaks.
WIP FOLDL_push_lab_thm
FOLD_push_lab_thm, and thoughts about cons_closure and emit_ec thms
add free_bods = [] hyp to compile_val, look at CFun case
prove thms about emit_ec and FOLDL_emit_ec

can't be sure that they are the correct theorems, though, since the
hypotheses need to be satisfied (ultimately by compile_val, but
proximately by compile_closures_thm). also thoughts about statement of
compile_closures_thm...
work towards cons_closure_thm
finish cons_closure_thm, start FOLDL_cons_closure_thm

However, want to simplify the representation of environments first: an
empty environment can be an empty block instead of a number since empty
blocks should be optimised at a lower level.
simplify representation of environments

now uniformly Block 0 [...]
finish a FOLDL_cons_closure_thm
more lemmas setting up for compile_closures_thm
work on num_fold_update_refptr_thm
work on num_fold_update_refptr_thm

getting something terribly wrong with the loop invariant... this is
harder than it ought to be.
more fiddling with num_fold_update_refptr_thm
finish num_fold_update_refptr_thm

required reasoning about all distinct refptrs after all...
finish num_fold_store_thm

ready to work on compile_closures_thm now
work on compile_closures_thm

probably need to relax some condition in FOLDL_cons_closure_thm for the
case when the closure is non-recursive and there are no RefPtrs...
more compile_closures_thm

might have the correct statement now
more compile_closures_thm

non-recursive case seems to work
bit more compile_closures_thm
finish a compile_closures_thm

now to see if it is sufficient for the CFun case...