Moved sorting of hypotheses from the SPARK VC parser to the point just
before paving is invoked.  Thus pp_simplify now preserves the order of
hypotheses.  Moreover, hypotheses sorting can now benefit problems not
coming from SPARK VCs.
Also fixed a number of issues with formatting of formulas and terms.