T:Type, L:T List, P:(TTProp).
  (x,y:T. Dec(P(x,y)))
  
  (x,y:T. P(x,y)  P(y,x))
  
  (L':T List. 
  ((L (swap adjacent[P(x,y)]^*) L') & (i:(||L'||-1). P(L'[i],L'[(i+1)])))

By:	Auto THEN Assert (Q:(TT). x,y:T. Q(x,y)  P(x,y))

1	1. T : Type 2. T List 3. P : TTProp 4. x,y:T. Dec(P(x,y)) 5. x,y:T. P(x,y)  P(y,x)   Q:(TT). x,y:T. Q(x,y)  P(x,y)	1 step
2	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). x,y:T. Q(x,y)  P(x,y)   L':T List.    (L (swap adjacent[P(x,y)]^*) L') & (i:(||L'||-1). P(L'[i],L'[(i+1)]))	8 steps

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