Def (L o f) == mklist(||L||;i.L[(f(i))])

is mentioned by

Thm* L:T List, f:(||L||||L||). ||(L o f)|| = ||L||	[permute_list_length]
Thm* L:T List, f:(||L||||L||), i:||L||. (L o f)[i] = L[(f(i))]	[permute_list_select]
Def swap(L;i;j) == (L o (i, j))	[swap]

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html