Def firstn(n;as)
Def == Case of as; nil  nil ; a.as'  if 0<n a.firstn(n-1;as') else nil fi
Def (recursive)

is mentioned by

Thm* as:T List, n:{0...||as||}, i:n. firstn(n;as)[i] = as[i]	[select_firstn]
Thm* as:A List, n:{0...||as||}. ||firstn(n;as)|| = n	[length_firstn]
Def as[m..n] == firstn(n-m;nth_tl(m;as))	[segment]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html