(2steps total)
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:
iseg
length
1
1.
T
: Type
2.
l1
:
T
List
3.
l2
:
T
List
4.
l
:
T
List
5.
l2
= (
l1
@
l
)
||
l1
||
||
l1
@
l
||
By:
RWO
Thm*
as
,
bs
:
T
List. ||
as
@
bs
|| = ||
as
||+||
bs
||
0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc