Def  {a:T} == {x:T| x = a  T }

is mentioned by

Thm*  B:(AType), f:(x:AB(x)). f  x:A{f(x):B(x)}	[range_restriction_dep]
Thm*  {a:{a:A}} =ext {a:A}	[singleton_singleton_self]
Thm*  x:{a:A}. x = a  {a:A}	[singleton_eq_in_self]

In prior sections: core

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html