in question is set to a pair, say (t4,c4) rather
than just t4, because we have to know how to interpret the
variables of t4.
<P>
There are situations where the terms being unified really do
share variables, for example when factoring the literals of
a clause; in those cases, you simply use the same context
for both terms.
<P>
When you call unify(), match(), or any other routine that
tries to make terms identical by instantiation, the terms you
give are not changed---all of the action happens in their contex