The headache an eGovernment might get from Prolog

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