1. T : Type
2. T List
3. u : T
4. v : T List
5. x:T. (x  v)  (l1,l2:T List. v = (l1 @ [x] @ l2))
6. x : T
7. l1 : T List
8. l2 : T List
9. [u / v] = (l1 @ [x] @ l2)
  x = u  (x  v)

1	5. x:T. (x  v)  (l1,l2:T List. v = (l1 @ [x / l2])) 6. x : T 7. l2 : T List 8. [u / v] = [x / l2]   x = u  (x  v)	1 step
2	5. x:T. (x  v)  (l1,l2:T List. v = (l1 @ [x / l2])) 6. x : T 7. u1 : T 8. v1 : T List 9. l2 : T List 10. [u / v] = [u1 / (v1 @ [x / l2])]   x = u  (x  v)	4 steps

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