 First-order unification

First-order unification seeks substitutions making first-order terms identical. Constructor decomposition and the occurs check produce a most general unifier when one exists.