WhoCites
Definitions
SimpleMulFacts
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Refl(
A
;
_1
,
_2
.
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
SimpleMulFacts
Sections
DiscrMathExt
Doc
a:T. E(a;a)T:Type, E:(T
TProp). Refl(T;x,y.E(x,y)) 
Propa:T. E(a;a)T:Type, E:(TTProp). Refl(T;x,y.E(x,y)) Prop
