UNIT-TRANSLATION ::= unit-translation UNIT-TERM RENAMING
A unit translation is written:
UT Rwhere the renaming R determines a mapping of symbols.
It allows some of the unit symbols to be renamed. [CHANGED:] Any symbols that happen to be shared by the renaming must be checked to originate from shared symbols in some unit. []