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. Any symbols that happen to be identified by the renaming must be checked to originate from the same symbol in some unit.