1. T : Type
2. P : L:(T List)(||L||-1)
3. m : (T List)
4. L:T List, i:(||L||-1).
4. P(L,i)  P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L)
5. L : T List
6. 0<||L||
7. f : (T List)(T List)
8. L:T List. 
8. f(L)
8. =
8. if null(L) L
8. else let i = search(||L||-1;P(L)) in if i=0 L else swap(L;i-1;i) fi fi
9. x : T List
10. i:(||x||-1). P(x,i)  P(swap(x;i;i+1),i) & m(swap(x;i;i+1))<m(x)
11. x = nil
12. 0<||x||
13. search(||x||-1;P(x)) = 0
  f(x) = swap(x;search(||x||-1;P(x))-1;search(||x||-1;P(x)))
  
  m(f(x))m(x) & (m(f(x)) = m(x)  f(x) = x)

By:	Assert (0search(||x||-1;P(x))-1 (& search(||x||-1;P(x))-1<||x||-1 (& P(x,search(||x||-1;P(x))-1))

1	0search(||x||-1;P(x))-1   & search(||x||-1;P(x))-1<||x||-1   & P(x,search(||x||-1;P(x))-1)	2 steps
2	14. 0search(||x||-1;P(x))-1 14. & search(||x||-1;P(x))-1<||x||-1 14. & P(x,search(||x||-1;P(x))-1)   f(x) = swap(x;search(||x||-1;P(x))-1;search(||x||-1;P(x)))      m(f(x))m(x) & (m(f(x)) = m(x)  f(x) = x)	3 steps

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