1. T : Type
2. x : T
3. T List
4. u : T
5. v : T List
6. l2:T List. (x  v @ l2)  (x  v)  (x  l2)
  l2:T List. (x  [u / (v @ l2)])  (x  [u / v])  (x  l2)

By:	RWW Thm* l:T List, a,x:T. (x  [a / l])  x = a  (x  l) 0

1	7. l2 : T List 8. x = u  (x  v @ l2)   x = u  (x  v)  (x  l2)	5 steps
2	7. l2 : T List 8. x = u  (x  v)  (x  l2)   x = u  (x  v @ l2)	5 steps

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