1. T : Type
2. T List
3. u : T
4. v : T List
5. b:T List. ||v|| = ||b||  (i:. i<||v||  v[i] = b[i])  v = b
6. T List
7. u1 : T
8. v1 : T List
9. ||[u / v]|| = ||v1||
9. 
9. (i:. i<||[u / v]||  [u / v][i] = v1[i])  [u / v] = v1
10. ||v||+1 = ||v1||+1
11. i:. i<||v||+1  [u / v][i] = [u1 / v1][i]
12. i : 
13. i<||v||
  v[i] = v1[i]

1

14. [u / v][(i+1)] = [u1 / v1][(i+1)]   v[i] = v1[i]

1 step

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