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. i<||l||
7. x = l[i]
  False

1

8. [x / l][0] = [x / l][(i+1)]   False

1 step

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