Unification should work on normal forms

[BinderDavid]

Currently the equations solved in the unifier are arbitrary expressions. We should change this so that unification only works on normal forms / neutral terms. If we generate a non-normal form by substitution in a constraint then we should immediately normalize that constraint.

The reason is that we probably want to implement Miller's pattern fragment of higher-order unification, and most presentations of that algorithm work on neutral terms which represent the application spine (or the destructor chain in our generalized system).