1. T : Type
2. L : T List
3. P : TTProp
4. x,y:T. Dec(P(x,y))
5. x,y:T. P(x,y)  P(y,x)
6. Q : TT
7. x,y:T. Q(x,y)  P(x,y)
8. L':T List. 
8. (L guarded_permutation(T;L,i. Q(L[i],L[(i+1)])) L')
8. & (i:(||L'||-1). Q(L'[i],L'[(i+1)]))
  L':T List. 
  (L (swap adjacent[P(x,y)]^*) L') & (i:(||L'||-1). P(L'[i],L'[(i+1)]))

1	8. L' : T List 9. guarded_permutation(T;L,i. Q(L[i],L[(i+1)]))(L,L')   (swap adjacent[P(x,y)]^*)(L,L')	2 steps
2	8. L' : T List 9. i:(||L'||-1). Q(L'[i],L'[(i+1)]) 10. i : (||L'||-1) 11. Q(L'[i],L'[(i+1)])   P(L'[i],L'[(i+1)])	2 steps

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