1. T : Type
2. T List
3. u : T
4. v : T List
5. l2:T List. v  l2  ||v||||l2|| & (i:. i<||v||  v[i] = l2[i])
6. T List
7. u1 : T
8. v1 : T List
9. [u / v]  v1
9. 
9. ||[u / v]||||v1|| & (i:. i<||[u / v]||  [u / v][i] = v1[i])
10. [u / v]  v1  (||[u / v]||||v1||
10. & (i:. i<||[u / v]||  [u / v][i] = v1[i]))
11. u = u1
12. v  v1
13. [u / v]  v1
13. 
13. ||[u / v]||||v1|| & (i:. i<||[u / v]||  [u / v][i] = v1[i])
14. [u / v]  v1  (||[u / v]||||v1||
14. & (i:. i<||[u / v]||  [u / v][i] = v1[i]))
15. ||v||||v1||
16. i:. i<||v||  v[i] = v1[i]
17. i : 
18. i<||v||+1
19. i = 0
  [u / v][i] = [u1 / v1][i]

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

None

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