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

is mentioned by

Thm*  B:({a:A}Type). (i:{a:A}B(i)) ~ B(a)	[card_sum_family_singleton_elim]
Thm*  (i:{a:A}B(i)) ~ B(a)	[card_prod_family_singleton_elim]
Thm*  a,a':. Thm*  a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) ~ ({a:}B(a)))	[card_sum_family_singleton_vs_intseg]
Thm*  a,a':. Thm*  a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a)))	[exteq_sum_family_singleton_vs_intseg]
Thm*  a,a':. Thm*  a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) =ext ({a:}B(a)))	[exteq_prod_family_singleton_vs_intseg]
Thm*  a,a':. a'-a = 1  ({a..a'} =ext {a:})	[exteq_singleton_vs_intseg]

In prior sections: core LogicSupplement

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