LEIBNIZ is a flag setting or other piece of information.
A flag setting for REWRITE-EQUALITIES.
When rewriting an equality (during a ND proof or when constructing
an etree), rewrite every equality using the Leibniz definition
[lambda x(A) lambda y(A) forall q(OA). q x implies q y]

TPS documentation homepage

© 1988-99, Carnegie Mellon University.

TPS homepage