mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
6Thm* L1,L2:T List, i,j:||L1||.
Thm* L2 = swap(L1;i;j)
Thm* 
Thm* L2[i] = L1[j] & L2[j] = L1[i] & ||L2|| = ||L1||   & L1 = swap(L2;i;j)
Thm* & (x:||L2||. x = i  x = j  L2[x] = L1[x])		[swapped_select]
cites the following:
4Thm* L:T List, i,j,x:||L||. swap(L;i;j)[x] = L[((i, j)(x))][swap_select]
3Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||  [swap_length]
5Thm* L1:T List, i,j:||L1||. swap(swap(L1;i;j);i;j) = L1[swap_swap]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb list 2 Sections MarkB generic Doc