thoughts towards evaluate_enveq

relation on source language values that says their environments are
equivalent (recursively), and theorem statement that starting with
equivalent environments one evaluates to equivalent results.
starting thoughts about enveq_v_to_Cv and exp_to_Cexp_syneq
make FV_def nicer, use separate constants for the list cases
work on exp_to_Cexp_syneq
prove syneq_exp_sym_no_labs

syneq is symmetric as long as there are no labels (the same would be
true if there were all labels. more generally, if the second
expression's labels are no more than the first's, but that would have
been harder to state and prove..)
up to finished Fun case of exp_to_Cexp_syneq
more exp_to_Cexp_syneq

attempting to simplify things by proving a syneq_exp_mkshift_both but
can't figure out the right statement
up to Mat case of exp_to_Cexp_syneq

and got syneq_exp_mkshift_both working
bit more exp_to_Cexp_syneq

ignoring Mat case for now - maybe the theorem statement can be changed
to make it easier though? looking at Letrec case, also seems like the
theorem statement might be slightly wrong there.
prove all but two cases of exp_to_Cexp_syneq

the pattern matching case probably will require a different statement
and more reasoning about remove_mat_var/vp. the other remaining case is
when consing on another def in a letrec.
use exp_to_Cexp_nice_ind instead, and get it down to 1 case

the nice_ind finesses the issue of consing onto the defs.
last case just looks to require proving syneq for remove_mat_var.
attempt at remove_mat_syneq stuff, not working

thinking might want to get rid of the z1 and z2 arguments of syneq_exp,
since they can probably just be represented by the V.
slightly simplify statement of exp_to_Cexp_syneq
managed to prove remove_mat_var_syneq
prove exp_to_Cexp_syneq
delete some unused stuff
start on enveq_v_to_Cv, probably need to strengthen exp_to_Cexp_syneq

start on proving a strengthened version... only want to have to relate
the first occurrence of a variable in the bvars list, since enveq will
only guarantee something about the first thing ALOOKUP finds.
prove stronger exp_to_Cexp_syneq
prove Closure case of enveq_v_to_Cv

Recclosure is next
prove enveq_v_to_Cv