In this lecture, we study term unification, substitution, most general unifier (m.g.u)
and unification algorithm.