(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
  T:Type, n:, f:(nT), i:n. mklist(n;f)[i] = f(i)
By: RepeatFor 2 (Analyze 0) THEN NatInd -1 THEN Reduce 0

Generated subgoals:

1 1. T : Type
  f:(0T), i:0. mklist(0;f)[i] = f(i)
Auto
2 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)
10 steps

About:
natural_numberapplyfunctionuniverseequalall
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