1. T : Type
2. n : 
3. 0<n
4. f:((n-1)T), i:(n-1). mklist(n-1;f)[i] = f(i)
  f:(nT), i:n. mklist(n;f)[i] = f(i)

1

5. f : nT 6. i:(n-1). mklist(n-1;f)[i] = f(i)   i:n. mklist(n;f)[i] = f(i)

9 steps

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