Committing the work on equality engine, I need to see how it does on the regressions...

Committing the work on equality engine, I need to see how it does on the regressions. New additions:
* areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later.
* propagation of shared dis-equalities (not yet complete, once case missing)
* changes to the theories that use it, authors should check up on the changes