Def a list xs == Case of xs; nil  False ; x.ys  x = a  A  a list ys
Def (recursive)

is mentioned by

Thm* f:(D:Type. D(D List)), A:Type, a,x:A. x list f(a)  x = a	[sfa_doc_type_poly_mem_const]
Thm* a:A, w:{a:A} List. z:A. z list w  z = a	[sfa_doc_inlist_singleton_const]

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