list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm* as,bs:T List, i:||as||. (as @ bs)[i] = as[i][select_append_front]
cites the following:
Thm* a:Tas:T List, i:i (a.as)[i] = a[select_cons_hd]
Thm* a:Tas:T List, i:. 0<i  i||as||  (a.as)[i] = as[(i-1)][select_cons_tl]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
list 1 Sections StandardLIB Doc