dimension action composition is broken for diagonals

[jonsterling]

This is something that was first noticed by favonia a while back, but I wanted to write it down so that we can theorize a fix. A diagonal dimension action [x = y] becomes either [y/x] or [x/y] depending on the total order of generic dimensions. But this information can cause the wrong thing to happen for composed substitutions.

Consider the following case:

   fix x0, x1, y where x0 < x1.

   [y / x1] o [x0 = x1]
   == [y / x1] o [x0 / x1]

On the other hand, suppose x1 > x0. then, we'd have

  [y / x1] o [x0 = x1]
  == [y / x1] o [x1 / x0]

The above would behave differently when applied to a term.

I think the problem is basically that we haven't really set any expectations about what composition of dimension substitutions should do. We should pick a semantics, and then ensure that all of redtt is sensible under that semantics.

[favonia]

Will be solved by #270, hopefully.