EXT : %THEOREM%
EXT
is a
theorem
.
Book
Theorem
:
FORALL
x(B) [f(
AB
) x
=
g(
AB
) x]
IMPLIES
f
=
g
Axiom of extensionality at all types.
TPS documentation homepage
© 1988-99, Carnegie Mellon University.
TPS homepage