Apply following law to a formula:

A equiv B --> (A implies B) and (B implies A).

The calling scheme for WFF-SUB-EQUIV is:

(WFF-SUB-EQUIV GWFF)

"GWFF"

The result is of type GWFF.

The arguments have the following meaning:

GWFF : Wff

© 1988-99, Carnegie Mellon University.