Def A List == {l:(A List)| (0<||l||) }

is mentioned by

Thm* A,B:Type, f:(AB), l:A List. map(f;l)  B List	[map_wf_listp]
Thm* l:A List. ||l||1	[listp_properties]

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