T:Type, P:(L:(T List)(||L||-1)), m:((T List)).
  (L:T List, i:(||L||-1).
  (P(L,i)  P(swap(L;i;i+1),i) & m(swap(L;i;i+1))<m(L))
  
  (L:T List. 
  (L':T List. 
  ((L guarded_permutation(T;L,i. P(L,i)) L') & (i:(||L'||-1). P(L',i)))

By:	Auto THEN Try (RWO Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L||   0)

1

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))

64 steps

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