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
,
l3
:
T
List.
l1
l2
l1
l2
@
l3
[iseg_append]
cites the following:
Thm*
as
,
bs
,
cs
:
T
List. ((
as
@
bs
) @
cs
) = (
as
@ (
bs
@
cs
))
[append_assoc]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
list
1
Sections
MarkB
generic
Doc
l1,l2,l3:T List. l1 
l2 
l1 l2 @ l3as,bs,cs:T List. ((as @ bs) @ cs) = (as @ (bs @ cs))l1,l2,l3:T List. l1 l2 l1 l2 @ l3as,bs,cs:T List. ((as @ bs) @ cs) = (as @ (bs @ cs))