def unify_walk(a, b, U):
    """
    unify_walk(a, b, U) returns an Unification where a and b are unified,
    given the unification that already exists in the Unification U. If the
    unification fails, it returns False.

    There are two ways to expand the functionality of unify_walk. The first way
    is:
    @comm_guard(type_of_a, type_of_b)
    def unify_walk(a, b, U):
        ...
    A function defined as such will be executed whenever the types of a and b
    match the declaration. Note that comm_guard automatically guarantees that
    your function is commutative: it will try to match the types of a, b or
    b, a.
    It is recommended to define unify_walk in that fashion for new types of
    Variable because different types of Variable interact a lot with each other,
    e.g. when unifying an OrVariable with a NotVariable, etc. You can return
    the special marker FALL_THROUGH to indicate that you want to relay execution
    to the next match of the type signature. The definitions of unify_walk are
    tried in the reverse order of their declaration.

    Another way is to override __unify_walk__ in an user-defined class.

    Limitations: cannot embed a Variable in another (the functionality could
    be added if required)

    Here is a list of unification rules with their associated behavior:

    """
    if a.__class__ != b.__class__:
        return False
    elif a == b:
        return U
    else:
        return False
