DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
IsEqFun(
b
;
i
,
j
.
i
=
j
)
[eq_int_is_eq_nsub]
cites the following:
Thm*
x
,
y
:
.
x
=
y
x
=
y
[assert_of_eq_int]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
b;
i,j. i=j)
x,y:
. x=y 
x = yb;i,j. i=j)x,y:. x=y x = y