+Free / :LambdaFree/[]>>Lambda. This is the same as
applying call/N on Lambda, except that only variables
appearing in Free are bound by the call. For example
p(1,a).
p(2,b).
?- {X}/p(X,Y).
X = 1;
X = 2.
This can in particularly be combined with bagof/3 and setof/3 to select particular variables to be concerned rather than using existential quantification (^/2) to exclude variables. For example, the two calls below are equivalent.
setof(X, Y^p(X,Y), Xs)
setof(X, {X}/p(X,_), Xs)