IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sublist tl21 1. T : Type
2. T List
3. u : T 4. v : T List
5. L2:T List. null(L2) v tl(L2) vL2 6. T List
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]