WhoCites
Definitions
HOLlib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites res
all?
res_all
Def res_all(
'a
;
x
.
P
(
x
);
x
.
Q
(
x
)) ==
x
:
'a
.
P
(
x
)
Q
(
x
)
Thm*
'a
:Type,
P
,
Q
:(
'a
Prop). res_all(
'a
;
x
.
P
(
x
);
x
.
Q
(
x
))
Prop
Syntax:
res_all(
'a
;
x
.
P
(
x
);
x
.
Q
(
x
))
has structure:
res_all(
'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_all('a;x.P(x);x.Q(x)) 
Propx:'a. P(x) Q(x)'a:Type, P,Q:('aProp). res_all('a;x.P(x);x.Q(x)) Prop
