T:Type, x,y:T, L:T List.
  (x  L)  (y  L)  x = y  x before y  L  y before x  L

1

1. T : Type 2. x : T 3. y : T 4. L : T List 5. i1 :  6. i1<||L|| 7. x = L[i1] 8. i :  9. i<||L|| 10. y = L[i]   x = y  [x; y]  L  [y; x]  L

10 steps

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