INSTANTIATE-EQUALITIES : WFFOPINSTANTIATE-EQUALITIES is a wff operation.
Instantiate all equalities in gwff. Consults the flag
REWRITE-EQUALITIES (but ignores it if it's set to NONE).
The calling scheme for INSTANTIATE-EQUALITIES is:
The result is of type GWFF.
The arguments have the following meaning:
INWFF : inwff
TPS documentation homepage