1. A : Type
2. l : A List
3. n : 
  l\[n]  A List

1	2. n :  3. n<0 4. l:A List. l\[n+1]  A List   l:A List. l\[n]  A List	1 step
2	l:A List. l\[0]  A List	1 step
3	2. n :  3. 0<n 4. l:A List. l\[n-1]  A List   l:A List. l\[n]  A List	7 steps

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