progress on compile_top_thm, single dec case

proved the bit about the invariant holding after the exception handler
is gone. (hopefully will be similar for the module case... extra
complication that the environment shifts over the menv.) next subgoal is
about the printed output...
finish first Tdec case of compile_top_thm