1. T : Type
2. T List
3. u : T
4. v : T List
5. L2:T List. null(L2)  v  tl(L2)  v  L2
6. L2 : T List
7. null(L2)
8. [u / v]  tl(L2)
  [u / v]  L2

1

7. u1 : T 8. v1 : T List 9. null(v1)  [u / v]  tl(v1)  [u / v]  v1 10. False 11. [u / v]  v1   [u / v]  [u1 / v1]

1 step

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