(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
1. T : Type
2. a : T
3. as : T List
4. i : 
5. 0<i
6. i||as||
  hd(nth_tl(i;a.as)) = as[(i-1)]
By: RWNth 1 (RecUnfoldTopC `nth_tl`) 0 THEN SplitOnConclITE

Generated subgoal:

1 7. 0<i
  hd(nth_tl(i-1;tl((a.as)))) = as[(i-1)]
2 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