WhoCites
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites union
to
sigma?
union_to_sigma
Def union_to_sigma(
e
) == InjCase(
e
;
a
. <0,
a
>;
b
. <1,
b
>)
Thm*
A
,
B
:Type. union_to_sigma
(
A
+
B
)
(
i
:
2
if
i
=
0
A
else
B
fi)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
A,B:Type. union_to_sigma 
(A+B)
(i:
2
if i=
0
A else B fi)A,B:Type. union_to_sigma (A+B)(i:2if i=0 A else B fi)
