(5steps 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:
compose
flips
append
1
1
1.
k
:
2.
L1
:
(
k
-1) List
3.
L2
:
(
k
-1) List
map(
i
.(
i
,
i
+1);
L1
@
L2
) ~ (map(
i
.(
i
,
i
+1);
L1
) @ map(
i
.(
i
,
i
+1);
L2
))
By:
BackThru
Thm*
f
,
as'
:Top,
A
:Type,
as
:
A
List. map(
f
;
as
@
as'
) ~ (map(
f
;
as
) @ map(
f
;
as'
))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc