Def Dec(P) == P  P

is mentioned by

Thm* Q:(Prop given P). Dec(P)  (P  Dec(Q))  Dec(P & Q)

[decidable__cand]

In prior sections: core int 1 bool 1 int 2

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