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
||
[iseg_length]
cites the following:
Thm*
as
,
bs
:
T
List. ||
as
@
bs
|| = ||
as
||+||
bs
||
[length_append]
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||||l2||as,bs:T List. ||as @ bs|| = ||as||+||bs|| 
l1,l2:T List. l1 l2 ||l1||||l2||as,bs:T List. ||as @ bs|| = ||as||+||bs||