Fix left-hand side unification

At the moment left-hand side unification is quite ad-hoc, which leads to errors such as injectivity in Noo.Logic.Equality (not every function f is injective). It would be cool to use the unifiers as equivalences approach from Cockx and Abel.