Unification is reflexive:

    (== x x) = x for all x

It is commutative:

    (== x y) = (== y x) for all x and y

It is idempotent:

    (== x (== x y)) = (== x y) for all x and y

And it is associative:

    (== x (== y z)) = (== (== x y) z)

It's not transitive, e.g. if we unify pairs (using made up syntax [a, b]) then

    (== [x, 1] [2, y]) = [2, 1]
    (== [2, y] [z, 3]) = [2, 3]
    (== [x, 1] [z, 3]) does not unify (since 1 does not unify with 3)