A flag setting for REWRITE-EQUALITIES.

When rewriting an equality (during a ND proof or when constructing

an etree), rewrite every equality as follows:

to an equivalence for those of type OOO,

to the extensional form

[lambda f(AB) lambda g(AB) forall x(B) f x = g x]

for those of type O(AB)(AB)

to the Leibniz form

[lambda x(A) lambda y(A) forall q(OA). q x implies q y]

for those of type OAA.

© 1988-99, Carnegie Mellon University.