DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
(
i
:{
a
:
A
}
B
(
i
)) ~
B
(
a
)
[card_prod_family_singleton_elim]
cites the following:
Thm*
x
:{
a
:
A
}.
x
=
a
{
a
:
A
}
[singleton_eq_in_self]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
B(i)) ~ B(a)
x:{a:A}. x = a 
{a:A}B(i)) ~ B(a)x:{a:A}. x = a {a:A}