(2steps total)
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
swap
length
T
:Type,
L
:
T
List,
i
,
j
:
||
L
||. ||swap(
L
;
i
;
j
)|| = ||
L
||
By:
Auto
Generated subgoal:
1
1.
T
: Type
2.
L
:
T
List
3.
i
:
||
L
||
4.
j
:
||
L
||
||swap(
L
;
i
;
j
)|| = ||
L
||
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc