Nuprl - list_1 LEMMAs for select_wf

list 1 Sections StandardLIB Doc

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

Theorem	Name
Thm* A:Type, l:A List, n:. 0n n<\|\|l\|\| l[n] A	[select_wf]
cites the following:
Thm* as:A List, n:{0...\|\|as\|\|}. \|\|nth_tl(n;as)\|\| = \|\|as\|\|-n	[length_nth_tl]

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

list 1 Sections StandardLIB Doc