Equivalence classes with canonical forms

[wwitzel]

We could make the automation more powerful by integrating equivalence classes into the concept of using canonical forms. Note that this would depend upon assumptions and what has been proven, so it would work differently than the canonical forms currently do. This needs to be thought out and may not be a priority for a while, but the idea has potential.