Formal Introduction to Unification