EPROOF-UTREE : UNIFOPEPROOF-UTREE is an unification command.
Create a new utree whose root has all the dpairs
associated with the current mating. (The existing utree may
have some of the dpairs added lower down the tree; this will
bring them all to the top). See also NAME-DPAIR.
The command format for EPROOF-UTREE is:
TPS documentation homepage