Can anyone please tell me why this fails?
f(X,X) = f(a,b).
It was my assumption that X would first be instantiated to a, then removed, then to b making just X = b. Trying it out, I see that I am wrong but I do not know why.
Thank you.
Unification always gives variables a consistent meaning. There is no value of X that makes f(X,X) = f(a,b) true. If you said
f(X) = f(a); f(X) = f(b).
Then you would get a result more like you are expecting.