Unification is a pure relation. It does not produce side effects and can be used in all directions, with either or both arguments fully or only partially instantiated.
In Prolog, unification can happen
explicitly, using built-in predicates like (=)/2 or unify_with_occurs_check/2
implicitly, whe...