Def Dec(P) == P  P

is mentioned by

Thm* P:(AProp). (x:A. Dec(P(x)))  (f:(A). x:A. P(x)  f(x))	[sfa_doc_bool_vs_decidable_fun]
Thm* Dec(P)  (b:. P  b)	[sfa_doc_bool_vs_decidable]

In prior sections: core int 1 bool 1 rel 1 int 2

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