mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
4
Thm*
x
,
y
:
T
.
x
before
y
nil
False
[nil_before]
cites the following:
3
Thm*
x
:
T
,
L
:
T
List. [
x
/
L
]
nil
False
[cons_sublist_nil]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
list
1
Sections
MarkB
generic
Doc
x,y:T. x before y 
nil 
Falsex:T, L:T List. [x / L] 
nil Falsex,y:T. x before y nil Falsex:T, L:T List. [x / L] nil False