Interesting.
However, unifiable/3 seems to be changed to keep
information so that the variable belong to which side.
% ?- unifiable(f(A, A, B), f(B, A, A), L).
%@ L = [B=A].
If we have L = [A-B, A-A, B-A], then we know L is not a bijection
to judge that f(A, A, B) and f(B, A, A) is not variant pair.
Unifiable performs the unification and then inspects the trail to find the unifications performed by this unification (and unbinds them again). If you inspect the code for unification and see how it deals with variable age, sharing and cycles, you’ll see there are no promises except that each term has the shape Var = Something.
Thank @jan W.
I think I understand your comment well, thanks,
though I was afraid my English is correct to tell what I had in mind to tell you.
I am not urgent, but I appreciate if someone will answer my naive question
on subsumes_term/2:
Is there any practical case in which ‘subsumes_term/2’ actually
is applied to shared pair of Generic and Specific like subsumes_term(A+B, B+A) ?
Even in such a case, renaming Specific is enough to avoid possible trouble ?
Short answer would be welcome.
I don’t know. I’ve never seen a practical case in my own coding, but that also applied to variant/2 
And yes, copying one of the sides might get the semantics you want. I would copy Generic, as it is likely to be smaller. I don’t know whether anyone in the ISO team considered sharing between the arguments or they had only single sided unification in mind. Neither do I know the current official text. Might be somewhere in Ulrich Neumerkels ISO archives.