Remark
WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
NOTE:
(
R
(_1;_2))(
a
,
b
)
is
alpha-equivalent
to
Symmetrize(
x
,
y
.
R
(
x
;
y
);
a
;
b
)
.
Who Cites symmetrize?
symmetrize
Def Symmetrize(
x
,
y
.
R
(
x
;
y
);
a
;
b
) ==
R
(
a
;
b
) &
R
(
b
;
a
)
Thm*
T
:Type{j},
R
:(
T
T
Prop{i}),
a
,
b
:
T
. Symmetrize(
x
,
y
.
R
(
x
,
y
);
a
;
b
)
Prop{i}
Syntax:
Symmetrize(
x
,
y
.
R
(
x
;
y
);
a
;
b
)
has structure:
symmetrize(
x
,
y
.
R
(
x
;
y
);
a
;
b
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Remark
WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
(R(_1;_2))(a,b)(R(_1;_2))(a,b)
T:Type{j}, R:(T
TProp{i}), a,b:T. Symmetrize(x,y.R(x,y);a;b) 
Prop{i}
