Def ||as|| == Case of as; nil  0 ; a.as'  ||as'||+1  (recursive)

is mentioned by

Thm* as:T List. (i.as[i]){||as||} = as	[sfa_doc_listify_select_id]
Thm* f:(D:Type. D(D List)), A:Type, a:A, B:Type, b:B. Thm* ||f(a)|| = ||f(b)||	[sfa_doc_type_poly_len_const]
Def y greater-bounds x == i:||x||. x[i]<y	[sfa_doc_greater_list_bound]

In prior sections: list 1

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html