is mentioned by

Thm* f:().  Thm* (n:. f(n) = 0) Thm*  Thm* (n:. if f(n)=0 False else C:Prop{1}. C fi)  Prop{1}	[sfa_doc_predicativity_sample8]
Thm* False  (C:Prop. C)	[sfa_doc_false_via_so]
Def a list xs == Case of xs; nil  False ; x.ys  x = a  A  a list ys Def (recursive)	[sfa_doc_inlist]

In prior sections: core bool 1

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html