Feature/substitution

Proper distinction between `Unifier` and `Substitution`.

Remind that a unifier is a substitution that satisfy certain conditions. If unifier is the most common type of substitution,  other substitutions are also considered (e.g. nullifiers, type propagating substitutions).

Some vocabulary changes:

- `Substitution` now refers to a substitution function.  Its previous restricted meaning has been moved to
`SingletonSubstitution`.
- The `Unifier` class has been mostly replaced by the `Substitution` class. Its static method `getMGU()` is now in `UnifierUtilities`.
- Static methods not specific to unification have been moved to `SubstitutionUtilities`.

New functionality:
- Union between substitutions has been implemented.