mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
L1
,
L2
:
T
List.
L1
=
L2
L1
L2
[sublist_weakening]
cites the following:
Thm*
k
:
. increasing(
i
.
i
;
k
)
[id_increasing]
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 
L2k:
. increasing(
i.i;k)L1,L2:T List. L1 = L2 L1 L2k:. increasing(i.i;k)