failed attempt at proving termination for exp_to_exh

will probably need a lexicographic measure