mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
3
Thm*
x
:
T
,
L
:
T
List. [
x
/
L
]
nil
False
[cons_sublist_nil]
cites the following:
2
Thm*
L1
,
L2
:
T
List.
L1
L2
||
L1
||
||
L2
||
[length_sublist]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
list
1
Sections
MarkB
generic
Doc
x:T, L:T List. [x / L] 
nil 
FalseL1,L2:T List. L1 L2 
||L1||
||L2||x:T, L:T List. [x / L] nil FalseL1,L2:T List. L1 L2 ||L1||||L2||