slightly strengthen compile_Cexp_thm

attempting to allow the new code to already be part of the assumed
invariant, to allow the call_repl_step theorem to go around in a loop.
but it looks like this is not going to lift easily up to the higher
level theorems (compile_fake_exp, compile_dec, etc.).