PrintForm
Definitions
Lemmas
LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
not
over
exists
imp
T
:Type,
Q
:(
T
Prop).
(
x
:
T
.
Q
(
x
))
(
x
:
T
.
Q
(
x
))
By:
RemoveGuards 0
THEN
SimilarTo:
Thm*
Q
:(
T
Prop).
(
x
:
T
.
Q
(
x
))
(
x
:
T
.
Q
(
x
))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
LogicSupplement
Sections
DiscrMathExt
Doc
T:Type, Q:(T
Prop). 
(
x:T. Q(x)) 
(x:T. Q(x)) T:Type, Q:(TProp). (x:T. Q(x)) (x:T. Q(x))Q:(TProp). (x:T. Q(x)) 
(x:T. Q(x))
