How to define a meta-logical predicate that tests (thus succeeds or fails only) if two lists of unique variables contain exactly the same variables using the built-ins from the current ISO standard (ISO/IEC 13211-1:1995 including Cor.2).
Stated differently, the predicate should succeed if one list of unique variables is a permutation of the other. In analogy to library(ordsets), let's call this meta-logical predicate varset_seteq(As, Bs).
Note that, in contrast to ord_seteq/2, this predicate cannot be simply As == Bs.
The solution I propose uses term_variables/2 to check if Bs has no extra variables over As and that As has no variable that doesn't appear in Bs.
varset_seteq(As, Bs):-
term_variables(As-Bs, As),
term_variables(Bs-As, Bs).
The above solution can be tricked to succeed with arguments that are not sets of free variables:
| ?- varset_seteq([A], [a]).
A = a
yes
To avoid that, unification can be replaced with equivalence test:
varset_seteq(As, Bs):-
term_variables(As-Bs, A0),
A0 == As,
term_variables(Bs-As, B0),
B0 == Bs.