(3steps total)
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
weakening
wrt
A
,
B
:Type.
A
=
B
(
A
~
B
)
By:
Def of
A
~
B
Generated subgoal:
1
1.
A
: Type
2.
B
: Type
3.
A
=
B
f
:(
A
B
),
g
:(
B
A
). InvFuns(
A
;
B
;
f
;
g
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
A,B:Type. A = B 
(A ~ B) A,B:Type. A = B (A ~ B) 
f:(A
B), g:(BA). InvFuns(A;B;f;g)
