(3steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card
union
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
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
A,B:Type. (A+B) ~ (B+A) A,B:Type. (A+B) ~ (B+A) 
f:((A+B)
(B+A)), g:((B+A)(A+B)). InvFuns(A+B;B+A;f;g)
