DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
k
:
,
j
:
k
. {
i
:
k
|
i
=
j
} ~
(
k
-1)
[nsub_delete_rw]
cites the following:
Thm*
k
:
,
j
:
k
,
m
:
.
m
=
k
-1
({
i
:
k
|
i
=
j
} ~
m
)
[nsub_delete]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
k:
, j:k. {i:k| 
i = j } ~ (k-1)k:, j:k, m:. m = k-1 
({i:k| i = j } ~ m)k:, j:k. {i:k| i = j } ~ (k-1)k:, j:k, m:. m = k-1 ({i:k| i = j } ~ m)