more work on type-declaration case of compile_dec_val
remove another cheat from compile_dec_val

also work on the last one, but it looks like it might require extending
the definition of all_cns... I need to be able to say that all the
constructor names appearing in an expression are in the domain of the
constructor environment to be able to say that it's OK to extend that
environment...
define new all_cns that also looks at constructors in expressions

and get semanticsExtraTheory building with this change
fix toIntLangProofsTheory for new all_cns
fix compile_fake_exp_val for new all_cns
extend all_cns again: forgot about cns in patterns
prove v_to_Cv_SUBMAP, allowing extending the constructor env
prove last cheat in compile_dec_val