8.1.2 Checking the Environ Section
In addition, we have to check the environ section. To do this, there are the
IRRVOC Checks unnecessary vocabulary.
IRRTHS Checks unnecessary theorems.
The method of using these is the same with the checking commands of the main section. For NOTATION and CONSTRUSTORS, there is no good way of checking. Therefore, use NOTATION and CONSTRUSTORS sparingly from the beginning and start with 0 and gradually include what is needed. However, if we accommodate after deleting an unnecessary file by IRRVOC, an error will appear in the NOTATION section, so we will be able to remove it.