\==/2
+Term1 \== +Term2
\==
Succeeds if Term1 and Term2 are non-identical terms.
term
None.
ref-lte-cte.