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

is mentioned by

Thm*  x:A. (x  nil)  False	[is_list_mem_null]
Thm*  x,a:A, ys:A List. (x  a.ys)  x = a  (x  ys)	[is_list_mem_split]
Def  xs == {a:A| a  xs }	[list_member_type]

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