mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
2
Thm*
L1
,
L2
:
T
List.
L1
L2
||
L1
||
||
L2
||
[length_sublist]
cites the following:
1
Thm*
k
,
m
:
. (
f
:(
k
m
). increasing(
f
;
k
))
k
m
[increasing_le]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
list
1
Sections
MarkB
generic
Doc
L1,L2:T List. L1 
L2 
||L1||
||L2||k,m:
. (
f:(k
m). increasing(f;k)) kmL1,L2:T List. L1 L2 ||L1||||L2||k,m:. (f:(km). increasing(f;k)) km