Def  True == 0  

is mentioned by

Thm*  (!A)  (!x:A. True)	[inhabited_uniquely_vs_exists_unique]
Thm*  (A)  (x:A. True)	[inhabited_vs_exists]

In prior sections: core bool 1

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