WhoCites
Definitions
HOLlib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites res
exists?
res_exists
Def res_exists(
'a
;
x
.
P
(
x
);
x
.
Q
(
x
)) ==
x
:
'a
.
P
(
x
) &
Q
(
x
)
Thm*
'a
:Type,
P
,
Q
:(
'a
Prop). res_exists(
'a
;
x
.
P
(
x
);
x
.
Q
(
x
))
Prop
Syntax:
res_exists(
'a
;
x
.
P
(
x
);
x
.
Q
(
x
))
has structure:
res_exists(
'a
;
x
.
P
(
x
);
x
.
Q
(
x
))
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
HOLlib
Sections
NuprlLIB
Doc
x:'a. P(x) & Q(x)
'a:Type, P,Q:('a
Prop). res_exists('a;x.P(x);x.Q(x)) 
Propx:'a. P(x) & Q(x)'a:Type, P,Q:('aProp). res_exists('a;x.P(x);x.Q(x)) Prop
