1. T : Type
2. l : T List
3. x : T
4. i,j:. i<||l||+1  j<||l||+1  i = j  [x / l][i] = [x / l][j]
5. i : 
6. j : 
7. i<||l||
8. j<||l||
9. i = j
10. [x / l][(i+1)] = [x / l][(j+1)]
  l[i] = l[j]

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

None

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