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:
permute
list
length
T
:Type,
L
:
T
List,
f
:(
||
L
||
||
L
||). ||(
L
o
f
)|| = ||
L
||
By:
Unfold `permute_list` 0
THEN
BackThru
Thm*
n
:
,
f
:(
n
T
). ||mklist(
n
;
f
)|| =
n
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc