Use lists of tuples for substitutions.

We used to used dictionaries for substitutions. Dictionaries, however, are
unordered. As a result, our unification algorithm was non-deterministic and
harder to analyse.