$$ \def\por{\ \ | \ \ } \def\dom{\textsf{dom}} \def\tsf#1{\textsf{#1}} \def\unifyj#1#2#3{#1 \sim #2 \Downarrow #3} \def\dict#1#2{\textsf{Dict}\left( #1, #2 \right)} \def\pf{\hookrightarrow}%\rightharpoonup \def\tone{{t_1}} \def\ttwo{{t_2}} \def\rule#1#2#3{\dfrac{#3}{#2}\ {#1}} \def\eqdef{\overset{\textsf{def}}{=}} \def\freevars{\textsf{free}} $$ Unification is probably one of the most important concepts in computer science. If you are not aware, unification is basically the process you undergo to find out how two syntactic objects like $a+b$ and $a+2c$ can be the same thing. In this case, you replace $b$ with $2c$.