Track known relations by canonical forms

[wwitzel]

Doing this properly should simplify transitive relation searches, making them more efficient. The idea would be to use canonical forms just for searching for known relations, equating things with the same canonical form as needed, but not allowing the actual form of the canonical forms to dictate the form the proof. That is, it shouldn't matter what the canonical forms are, as long as they form proper equivalence classes.