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

1

5. f : nT 6. ||mklist(n-1;f)|| = n-1     ||mklist(n;f)|| = n

3 steps

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