Nuprl - mb_list_2 LEMMAs for permute_list_select

mb list 2 Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
3	Thm* L:T List, f:(\|\|L\|\|\|\|L\|\|), i:\|\|L\|\|. (L o f)[i] = L[(f(i))]	[permute_list_select]
cites the following:
2	Thm* n:, f:(nT), i:n. mklist(n;f)[i] = f(i)	[mklist_select]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb list 2 Sections MarkB generic Doc