PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
iseg
nil
T
:Type,
L
:
T
List.
L
nil
null(
L
)
By:
Unfold `iseg` 0 THEN ObviousListInduction
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc
T:Type, L:T List. L 
nil 
null(L) T:Type, L:T List. L nil null(L)
