PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
function
functionality
wrt
one
one
corr
A
,
A'
,
B
,
B'
:Type. (
A
~
A'
)
(
B
~
B'
)
((
A
B
) ~ (
A'
B'
))
By:
BackChain:
Thm*
(
x
:
A
.
B
(
x
)) ~ (
x
:
A'
.
B'
(
x
))
((
x
:
A
B
(
x
)) ~ (
x
:
A'
B'
(
x
))) |
Thm*
(
A
~
A'
)
(
B
~
B'
)
(
:
A
.
B
) ~ (
:
A'
.
B'
)
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') 
B) ~ (A'
