WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
NOTE:
Refl(
A
)(
R
(_1;_2))
is
alpha-equivalent
to
Refl(
A
;
x
,
y
.
R
(
x
;
y
))
.
Who Cites refl?
refl
Def Refl(
T
;
x
,
y
.
E
(
x
;
y
)) ==
a
:
T
.
E
(
a
;
a
)
Thm*
T
:Type,
E
:(
T
T
Prop). Refl(
T
;
x
,
y
.
E
(
x
,
y
))
Prop
Syntax:
Refl(
T
;
x
,
y
.
E
(
x
;
y
))
has structure:
refl(
T
;
x
,
y
.
E
(
x
;
y
))
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc