Clean up EquivalenceClass
Clean up EquivalenceClass

Now there's documentation, and the proofs are slightly better automated.

CategoricalData/catdb,CategoricalData/catdb,JasonGross/catdb,JasonGross/catdb