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
7. n = 0
  ||(i,l. l @ [(f(i))])(n-1,primrec(n-1;nil;i,l. l @ [(f(i))]))|| = n  

By:	Reduce 0 THEN Fold `mklist` 0 THEN RWO Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||   0

None

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