T:Type, L1,L2:T List, i,j:||L1||.
  L2 = swap(L1;i;j)
  
  L2[i] = L1[j] & L2[j] = L1[i] & ||L2|| = ||L1||   & L1 = swap(L2;i;j)
  & (x:||L2||. x = i  x = j  L2[x] = L1[x])

1

1. T : Type 2. L1 : T List 3. L2 : T List 4. i : ||L1|| 5. j : ||L1|| 6. L2 = swap(L1;i;j)   L2[i] = L1[j] & L2[j] = L1[i] & ||L2|| = ||L1||   & L1 = swap(L2;i;j)   & (x:||L2||. x = i  x = j  L2[x] = L1[x])

2 steps

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