prove the easy cheats in prompt_to_i2_correct

the remaining cheats are about re-establishing the envC_tagged
invariant. it is not obvious whether that is possible.