1. A : Type
2. A List
3. u : A
4. v : A List
5. n:. firstn(n;v)  A List
6. n : 
  if 0<n u.firstn(n-1;v) else nil fi  A List

1	7. 0<n   u.firstn(n-1;v)  A List	3 steps
2	7. n0   nil  A List	Auto

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