LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
F
:(Prop
Prop). (
P
:Prop.
F
(
P
))
(
A
:Type.
F
(
A
))
[inhab_rep_eqv]
cites the following:
Thm*
A
:Type.
P
= (
A
)
Prop
[inhab_rep_axiom]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
LogicSupplement
Sections
DiscrMathExt
Doc
F:(Prop
Prop). (P:Prop. F(P)) 
(A:Type. F(
A))A:Type. P = (A) PropF:(PropProp). (P:Prop. F(P)) (A:Type. F(A))A:Type. P = (A) Prop