update proof about compile_fake_exp

simpler now because it either just goes to the end of the code (success)
leaving a new stack satisfying env_rs, or jumps to address 0 with the
old stack plus an exception on top.