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
inversion
A
,
B
:Type. (
A
~
B
)
(
B
~
A
)
By:
Def of Sym
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:Type. (A ~ B) 
(B ~ A) A,B:Type. (A ~ B) (B ~ A)
Def of Sym x,y:Type. x ~ y THEN BackThru: Thm* EquivRel X,Y:Type. X ~ Y
