Unifier works in a slightly more consistent way

* The current code jumbles up substitution with adding/deleting equations *way*
  too much. This clears up a bit of that in the process of fixing an inference bug