rework statement of prompt_to_i2_correct

remove the hypothesis about FDOMs of exhs being DISJOINT, but strengthen
the assumptions about what the prompts can look like. (also the
to_i2_invariant has been augmented.)