CLEANUP : MEXPRCLEANUP is a top-level command.
If the proof is complete, will delete unnecessary lines
from a proof. It may also eliminate or suggest eliminating
If the proof is incomplete, will do a partial cleanup in which
only unnecessary lines justified by SAME will be removed.
The command format for CLEANUP is:
TPS documentation homepage