PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
one
one
corr
2
transitivity
A
,
B
,
C
:Type. (
A
~
B
)
(
B
~
C
)
(
A
~
C
)
By:
Def of Trans
X
,
Y
:Type.
X
~
Y
THEN BackThru:
Thm*
EquivRel
X
,
Y
:Type.
X
~
Y
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
A,B,C:Type. (A ~ B) 
(B ~ C) (A ~ C) A,B,C:Type. (A ~ B) (B ~ C) (A ~ C)
Def of Trans X,Y:Type. X ~ Y THEN BackThru: Thm* EquivRel X,Y:Type. X ~ Y
