(6steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select append back 1
1. T : Type
2. as : T List
3. bs : T List
4. i : {||as||..(||as||+||bs||)}
  (as @ bs)[i] = bs[(i-||as||)]
By: ListInd 2 THEN AbReduce 0 THEN Analyze 0

Generated subgoals:

1 4. i : (0+||bs||)
  bs[i] = bs[(i-0)]
Auto
2 4. u : T
5. v : T List
6. i:{||v||..(||v||+||bs||)}. (v @ bs)[i] = bs[(i-||v||)]
7. i : {(||v||+1)..(||v||+1+||bs||)}
  (u.(v @ bs))[i] = bs[(i-(||v||+1))]
3 steps

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

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