1. T : Type
2. T List
3. u : T
4. v : T List
5. ||v||  0
6. x:T, L':T List. v = (L' @ [x])
  0<||[u / v]||  (x:T, L':T List. [u / v] = (L' @ [x]))

1

6. x : T 7. L' : T List 8. v = (L' @ [x]) 9. 0<||[u / v]||   [u / v] = ([u / L'] @ [x])

1 step

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