(5steps total) PrintForm Definitions list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select cons tl 1

1. T : Type
2. a : T
3. as : T List
4. i : 
5. 0<i
6. i||as||
  (a.as)[i] = as[(i-1)]


By: RWN 1 (UnfoldTopC `select`) 0 THEN AbReduce 0


Generated subgoal:

1   hd(nth_tl(i;a.as)) = as[(i-1)]
3 steps

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

(5steps total) PrintForm Definitions list 1 Sections StandardLIB Doc