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
functionality
wrt
one
one
corr
A
,
A'
,
B
,
B'
:Type. (
A
~
A'
)
(
B
~
B'
)
((
A
~
B
)
(
A'
~
B'
))
By:
Auto THEN ChainRelation:
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,A',B,B':Type. (A ~ A') 
(B ~ B') ((A ~ B) 
(A' ~ B')) A,A',B,B':Type. (A ~ A') (B ~ B') ((A ~ B) (A' ~ B'))
