WhoCites
Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Trans
_1
,
_2
:
A
.
R
(
_1
;
_2
)
is
alpha-equivalent
to
Trans
x
,
y
:
A
.
R
(
x
;
y
)
.
Who Cites trans?
trans
Def Trans
x
,
y
:
T
.
E
(
x
;
y
) ==
a
,
b
,
c
:
T
.
E
(
a
;
b
)
E
(
b
;
c
)
E
(
a
;
c
)
Thm*
T
:Type,
E
:(
T
T
Prop). (Trans
x
,
y
:
T
.
E
(
x
,
y
))
Prop
Syntax:
Trans
x
,
y
:
T
.
E
(
x
;
y
)
has structure:
trans(
T
;
x
,
y
.
E
(
x
;
y
))
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
LogicSupplement
Sections
DiscrMathExt
Doc
a,b,c:T. E(a;b) 
E(b;c) E(a;c)T:Type, E:(T
TProp). (Trans x,y:T. E(x,y)) 
Propa,b,c:T. E(a;b) E(b;c) E(a;c)T:Type, E:(TTProp). (Trans x,y:T. E(x,y)) Prop
