(2steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card
product
swap
A
,
B
:Type. (
A
B
) ~ (
B
A
)
By:
Def of <type> ~ <type>
Generated subgoal:
1
1.
A
: Type
2.
B
: Type
f
:(
A
B
B
A
),
g
:(
B
A
A
B
). InvFuns(
A
B
;
B
A
;
f
;
g
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
A,B:Type. (A
B) ~ (BA) A,B:Type. (AB) ~ (BA) 
f:(AB
BA), g:(BAAB). InvFuns(AB;BA;f;g)
