prove cheats in exh_disjoint2

this makes prog_to_i2_correct cheat-free