prove evaluate_prompt_i2_exh_weak

needed to add assumption about non-type-error
remove unnecessary assumption from prompt_to_i2_correct

this is perhaps a bad sign: we don't need to assume that a prompt of
SOME mn only makes declarations of things with module mn.