LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
Q
:Prop(given
P
). Dec(
P
)
(
P
Dec(
Q
))
Dec(
P
&
Q
)
[decidable__cand]
cites the following:
Thm*
Q
:Prop(given
P
).
P
Q
Prop
[guarded_prop_to_prop]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
LogicSupplement
Sections
DiscrMathExt
Doc
Q:Prop(given P). Dec(P) 
(P Dec(Q)) Dec(P & Q)Q:Prop(given P). P Q 
PropQ:Prop(given P). Dec(P) (P Dec(Q)) Dec(P & Q)Q:Prop(given P). P Q Prop