LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
(
x
:
T
.
Q
(
x
))
(
x
:
T
.
Q
(
x
))
[not_over_exists_imp]
cites the following:
Thm*
Q
:(
T
Prop).
(
x
:
T
.
Q
(
x
))
(
x
:
T
.
Q
(
x
))
[not_over_exists]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
LogicSupplement
Sections
DiscrMathExt
Doc
(
x:T. Q(x)) 
(
x:T. Q(x))Q:(T
Prop). (x:T. Q(x)) 
(x:T. Q(x))(x:T. Q(x)) (x:T. Q(x))Q:(TProp). (x:T. Q(x)) (x:T. Q(x))