WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites strict
part?
strict_part
Def strict_part(
x
,
y
.
R
(
x
;
y
);
a
;
b
) ==
R
(
a
;
b
) &
R
(
b
;
a
)
Thm*
T
:Type,
R
:(
T
T
Prop),
a
,
b
:
T
. strict_part(
x
,
y
.
R
(
x
,
y
);
a
;
b
)
Prop
not
Def
A
==
A
False
Thm*
A
:Prop. (
A
)
Prop
Syntax:
strict_part(
x
,
y
.
R
(
x
;
y
);
a
;
b
)
has structure:
strict_part(
x
,
y
.
R
(
x
;
y
);
a
;
b
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc