is mentioned by
 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] |
L1,L2,L:T List. disjoint_sublists(T;L1;L2;L) L1  L & L2 L | [disjoint_sublists_sublist] |
In prior sections: core well fnd int 1 bool 1 int 2 rel 1 num thy 1 list 1 mb nat mb list 1 sqequal 1
Try larger context:
MarkB generic
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html