retrieves values through levels of variable bindings

Unify is called with three arguments:

  (unify (level-x x) (level-y y) env)

If x and y don't match, unify returns nil. Otherwise, it returns a
new environment, which is the old one with possible new bindings
pushed on top.

The unification algorithm is a version of the algorithm described
in detail in "LOGLISP: Motivation, Design and Implementation"
by J.A.Robinson and E.E.Sibert (1984).