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

is mentioned

In prior sections: DiscreteMath

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