1. T : Type
2. L : T List
3. x : T
4. i : {1..(||L||+1)}
5. j : {1..(||L||+1)}
6. i1 : 
7. i1<||swap([x / L];i;j)||
8. i1 = 0
  swap([x / L];i;j)[i1] = [x / swap(L;i-1;j-1)][i1]

By:	RWO Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)] 0

1	i1||swap(L;i-1;j-1)||	1 step
2	swap([x / L];i;j)[i1] = swap(L;i-1;j-1)[(i1-1)]	6 steps

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