Def True == 0  

is mentioned by

Thm* eq:EqDecider(A), x:A, v,P:Top. z != x : v(x) ==> P(a,z) ~ (True  P(x,v))

[fpf-val-single1]

In prior sections: core mb list 1 bool 1

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