(12steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: listify select id 1 1
1. T : Type
2. as : T List
3. n : 
4. j : 
5. j+||as|| = n
  (i.as[(i-j)]){j..n} = as
By: MoveToConcl 4 THEN ListInd 2 THEN AbReduce 0 THEN UnivCD

Generated subgoals:

1 5. j+0 = n
  (i.nil[(i-j)]){j..n} = nil  T List
1 step
2 4. u : T
5. v : T List
6. j:. j+||v|| = n  (i.v[(i-j)]){j..n} = v
7. j : 
8. j+||v||+1 = n
  (i.(u.v)[(i-j)]){j..n} = u.v
7 steps

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

(12steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc