WhoCites
Definitions
HOLlib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites one
one?
one_one
Def one_one(
'a
;
'b
;
f
) ==
x
,
y
:
'a
.
f
(
x
) =
f
(
y
)
'b
x
=
y
Thm*
'a
,
'b
:Type,
f
:(
'a
'b
). one_one(
'a
;
'b
;
f
)
Prop
Syntax:
one_one(
'a
;
'b
;
f
)
has structure:
one_one(
'a
;
'b
;
f
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
HOLlib
Sections
NuprlLIB
Doc
x,y:'a. f(x) = f(y) 
'b 
x = y'a,'b:Type, f:('a
'b). one_one('a;'b;f) Propx,y:'a. f(x) = f(y) 'b x = y'a,'b:Type, f:('a'b). one_one('a;'b;f) Prop
