prove termination for exp_to_exh

needed to define a different size function with enough slop to
accommodate the extra things added to pattern matches by add_default.