1. T : Type
2. a : T List
3. b : T List
4. ||a|| = ||b||
5. i:. i<||a||  a[i] = b[i]
  a = b

1

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]   [u / v] = [u1 / v1]

5 steps

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