more lemmas, and work on compile_decs_thm

also still strengthening compile_fake_exp_thm
prove error case of compile_decs_thm

the difficulty has been dealing with the changing contab and cenv, i.e.
figuring out what to put in the statement for which contab and cenv to
use for the exception case. not sure if it's good enough, but using the
final cenv (as if all declarations had gone through, and computed
separately) for this theorem statement. intuitively that matches the
semantics...