prove cheats up to work point in exp_to_exh_correct