possible bug fix in definition of prompt_to_i2

discard the new tagenv produced by decs_to_i2.

(Also, the generated script files are slightly changed due to a Lem
update.)
strengthen definition of flat_envC_tagged

add extra condition that is in envC_tagged but wasn't in the flat
version previously.
prove one of the cheats in prompt_to_i2_correct