T:Type, L:T List, P:(TT).
  (x,y:T. P(x,y)  P(y,x))
  
  (L':T List. 
  ((L guarded_permutation(T;L,i. P(L[i],L[(i+1)])) L')
  (& (i:(||L'||-1). P(L'[i],L'[(i+1)])))

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

1

1. T : Type 2. L : T List 3. P : TT 4. x,y:T. P(x,y)  P(y,x)   L':T List.    (L guarded_permutation(T;L,i. P(L[i],L[(i+1)])) L')   & (i:(||L'||-1). P(L'[i],L'[(i+1)]))

7 steps

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