Some progress on conLang.
Reduce a cheat
Merge remote-tracking branch 'origin/master' into conLang_wip
Merge branch 'master' into conLang_wip
prove exhaustive_env_weak
correct a type annotation
tiny look at decs_to_i2_correct
move compilerLib to compiler subdir
make exh_ctors_env use a set type rather than a list

but use finite maps from nat to unit rather than lem sets, since we want
to be able to translate them. this is a placeholder type until we start
using an efficient representation for sets of nats. (abstract out the
nat_set type and operations to facilitate a change later.)

proofs not updated.
fix decLangProof for change to exh type
fix exhLangProof for change to exh type
switch to sptrees instead of num |-> unit

because this enables removing comparison of HOL sets, which won't
translate

proofs not updated
fix decLangProof for change to sptrees
fix exhLangProof for switch to sptree
start updating conLangProof
prove exhaustive_env_weakened_exh_SUBMAP

and bit of work trying to push conLang forward, not getting far
prove cenv_inv_to_mod
minor bug fix in lift_conjunct_conv
possible progress on decs_to_i2_correct
pushing on decs_to_i2_correct

looks like there might be an issue with the semantics of
evaluate_decs_i1; also maybe cenv_inv_to_mod is too weak (should it be
using build_exh_env?).