1. T : Type
2. n : 
3. 0<n
4. f:((n-1)T). ||mklist(n-1;f)|| = n-1
5. f : nT
6. ||mklist(n-1;f)|| = n-1
  ||mklist(n;f)|| = n  

1	7. n = 0   ||nil|| = n	Auto
2	7. n = 0   ||(i,l. l @ [(f(i))])(n-1,primrec(n-1;nil;i,l. l @ [(f(i))]))|| = n	1 step

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