1. T : Type
2. n : 
3. 0<n
4. f:((n-1)T), i:(n-1). mklist(n-1;f)[i] = f(i)
5. f : nT
6. i:(n-1). mklist(n-1;f)[i] = f(i)
7. n = 0
8. i : n
9. i<n-1
  (mklist(n-1;f) @ [(f(n-1))])[i] = f(i)

By:	Subst' (i = n-1) 0 THEN RWO Thm* as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)] 0 THEN Subst' (||mklist(n-1;f)|| = n-1) 0 THEN Try (BackThru Thm* n:, f:(nT). ||mklist(n;f)|| = n  )

1

[(f(n-1))][(n-1-(n-1))] = f(n-1)

1 step

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