is mentioned by

Thm*  x:A. (x  nil)  False	[is_list_mem_null]
Def  a  xs == Case of xs; nil  False ; x.ys  a = x  A  (a  ys) Def  (recursive)	[is_list_mem]

In prior sections: core bool 1 IteratedBinops

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