From: janburse@fastmail.fm   
      
   Hi,   
      
   That false/0 and not fail/0 is now all over the place,   
   I don't mean in person but for example here:   
      
   ?- X=f(f(X), X), Y=f(Y, f(Y)), X = Y.   
   false.   
      
   Is a little didactical nightmare.   
      
   Syntactic unification has mathematical axioms (1978),   
   to fully formalize unifcation you would need to   
   formalize both (=)/2 and (≠)/2 (sic!), otherwise you   
   rely on some negation as failure concept.   
      
   Keith L. Clark, Negation as Failure   
   https://link.springer.com/chapter/10.1007/978-1-4684-3384-5_11   
      
   You can realize a subset of a mixture of (=)/2   
   and (≠)/2 in the form of a vanilla unify Prolog   
   predicate using some of the meta programming   
   facilities of Prolog, like var/1 and having some   
      
   negation as failure reading:   
      
   /* Vanilla Unify */   
   unify(V, W) :- var(V), var(W), !, (V \== W -> V = W; true).   
   unify(V, T) :- var(V), !, V = T.   
   unify(S, W) :- var(W), !, W = S.   
   unify(S, T) :- functor(S, F, N), functor(T, F, N),   
         S =.. [F|L], T =.. [F|R], maplist(unify, L, R).   
      
   I indeed get:   
      
   ?- X=f(f(X), X), Y=f(Y, f(Y)), unify(X,Y).   
   false.   
      
   If the vanilla unify/2 already fails then unify   
   with and without subject to occurs check, will also   
   fail, and unify with and without ability to   
   handle rational terms, will also fail:   
      
   Bye   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)