To unify two items simply use =/2, which is defined as if by
the clause
=(X, X).
Please note: Do not confuse this predicate with
=:=/2(arithmetic comparison) or==/2(term identity).
Term subsumption is a sort of one-way unification. Term S and T unify if they have a common instance, and unification in Prolog instantiates both terms to that common instance. S subsumes T if T is already an instance of S. For our purposes, T is an instance of S if there is a substitution that leaves T unchanged and makes S identical to T.
Subsumption is checked by subsumes_chk/2. It is especially
useful in applications such as theorem provers. The built-in
predicate behaves identically to the original library version but is
much more efficient.
Related predicates are defined in library(subsumes) and
library(occurs). (For information on these packages see
lib).