Nuprl - mb_list_2 LEMMAs for permute_list_length

mb list 2 Sections MarkB generic Doc

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

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

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

mb list 2 Sections MarkB generic Doc