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