implement JRH's term ordering and prove equivalent to current ACONV

I believe John Harrison's latest (or maybe it is in progress) kernel for
HOL Light uses a term ordering along the lines defined here (I am
copying definitions from him) to test terms for alpha-equivalence but
also to maintain sets with canonical representations as lists (by
sorting) for hypotheses on theorems.

The plan is eventually to use this ordering, or something like it, for
our model of the inference system too. This might also help with the
conservativity proof, where the order (and even duplicate elements) of
hypothesis list elements was causing problems. It will certainly help
with proving derived rules for our inference system.

Equivalence with the current ACONV is a sanity check on the definitions.
It might also be the basis for avoiding a lot of proof updating if the
inference system changes (but not sure if that will work out...).