(12steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: mklist select 2 1 2 1 1

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: RWO Thm* as,bs:T List, i:||as||. (as @ bs)[i] = as[i] 0


Generated subgoals:

1   i<||mklist(n-1;f)||
1 step
2   mklist(n-1;f)[i] = f(i)
1 step

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

(12steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc