Implement equation-level check for need of unification

[xblahoud]

SESystems with simple equations (with no variable repetitions) are always trivially unified, regardless the constraints on variables. It's cheaper to check whether system is unified on equation in comparison to on automata.

• add boolean field needs_unification to equations
• check repetition of variables in equation constructor
• add checks for need_unification in code where appropriete
  1. at calls to is_unified and unify only, or
  2. whenever we are calling these functions