PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nil
before
T
:Type,
x
,
y
:
T
.
x
before
y
nil
False
By:
((Unfold `l_before` 0) THEN (RWO
Thm*
x
:
T
,
L
:
T
List. [
x
/
L
]
nil
False 0))
THEN
SimpConcl
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
T:Type, x,y:T. x before y 
nil 
False T:Type, x,y:T. x before y nil Falsex:T, L:T List. [x / L] 
nil False 0))
