dif/2 is a constraint that is true only if both of its arguments are different terms.
True iff X and Y are different terms. Unlike
dif/2 is more declarative because if X and Y can unify but they're not yet equal, the decision is delayed, and prevents X and Y to become equal later. Examples:
?- dif(a, a). false. ?- dif(a, b). true. ?- dif(X, b). dif:dif(X,b). ?- dif(X, b), X = b. false.