IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
partial sort exists1 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
L':T List.
(L guarded_permutation(T;L,i. P(L,i)) L') & (i:(||L'||-1). P(L',i))