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]  [u1 / v1]
  ||v||+1||v1||+1 & (i:. i<||v||+1  [u / v][i] = [u1 / v1][i])

By:	RWW Thm* a,b:T, l1,l2:T List. [a / l1]  [b / l2]  a = b & l1  l2 -1 THEN Analyze -1 THEN AllHyps (InstHyp [v1])

1

10. u = u1 11. v  v1 12. [u / v]  v1 12.  12. ||[u / v]||||v1|| & (i:. i<||[u / v]||  [u / v][i] = v1[i]) 13. v  v1  ||v||||v1|| & (i:. i<||v||  v[i] = v1[i])   ||v||+1||v1||+1 & (i:. i<||v||+1  [u / v][i] = [u1 / v1][i])

4 steps

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