prove a version of prompt_to_i2_correct

A cheat-free version of this theorem (for once). Uses the old envC in
the case of an exception, so it might require some tweaks further up in
compile_top/prog's theorems. Not sure if all the assumptions on this
prompt_to_i2_correct are strictly necessary.