(4steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
set
functionality
wrt
one
one
corr
n
pred2
1
1
1.
A
: Type
2.
B
:
A
Prop
3.
B'
:
A
Prop
4.
x
:
A
.
B
(
x
)
B'
(
x
)
Bij(
A
;
A
; Id)
By:
Use:[
g
:= Id]
BackChain:
Thm*
InvFuns(
A
;
B
;
f
;
g
)
Bij(
A
;
B
;
f
) |
Thm*
InvFuns(
A
;
A
;Id;Id)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
Prop
x:A. B(x) 
B'(x)
Bij(A; A; Id)
