core StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
TheoremName
Thm* (P  Q (Dec(P Dec(Q))[decidable_functionality]
cites the following:
Thm* Dec(A (A  B Dec(B)[iff_preserves_decidability]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
core StandardLIB Doc