LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
{
a
:{
a
:
A
}} =ext {
a
:
A
}
[singleton_singleton_self]
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
LogicSupplement
Sections
DiscrMathExt
Doc
x:{a:A}. x = a 
{a:A}x:{a:A}. x = a {a:A}