Bug Fix: do not simplify disequalities.

The code in ArrayTheory assumes, that the weak congruence will
simply use the index disequalities as is.  Otherwise the unit clauses
will not be unit clauses.  TODO: still have to check that the
propagated equality agrees between array theory and weak congruence
path.

Also the generated lemma was buggy, if the shared term disequality
simplified to false:  The equalities that lead to the shared terms
were missing.