EXT-LEIB : %THEOREM%

EXT-LEIB is a theorem.
Book Theorem:
FORALL f(AB) FORALL g(AB) .FORALL x(B) [f x = g x] IMPLIES FORALL q(O(AB)) .q f IMPLIES q g
Extensional equality of f and g implies Leibniz equality of f and g.

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage