Solver for Linear Equalities
extending the normal form definition to include sums of literals:
modifying unification to perform variable elimination (on normalized expressions)
We do not define an equality predicate, but rather handle linear equalities by