LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
(
A
:Type,
Q
:(
A
A
Prop).
P
:(
A
Prop).
p
:
A
.
x
:
A
.
Q
(
x
,
p
)
P
(
x
))
[RussellsParadox_Frege]
cites the following:
Thm*
(
P
P
)
[no_prop_iff_its_neg]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
LogicSupplement
Sections
DiscrMathExt
Doc
(
A:Type, Q:(A
AProp). 
P:(AProp). p:A. x:A. Q(x,p) 
P(x))(P P)(A:Type, Q:(AAProp). P:(AProp). p:A. x:A. Q(x,p) P(x))(P P)