rework statement of compile_decs_thm

Don't assume env_rs of the "initial state" to which an exception might
return. Just prove lots of stuff about the store in the exception case,
so as to defer the problem of proving the invariant in the old
environment and new store to whoever actually has the invariant at hand
(i.e. a later theorem, probably for compile_decs_wrap).

Also reduce the proof to two large but plausible cheats.