(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. T : Type
2. as : T List
  (i:||as||. as[i]){||as||} = as
By: Assert (n,j:. j+||as|| = n  (i.as[(i-j)]){j..n} = as) THENA UnivCD

Generated subgoals:

1 3. n : 
4. j : 
5. j+||as|| = n
  (i.as[(i-j)]){j..n} = as
9 steps
2 3. n,j:. j+||as|| = n  (i.as[(i-j)]){j..n} = as
  (i:||as||. as[i]){||as||} = as
1 step

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

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