Def  T == {:True| T }

is mentioned by

Thm*  {x:A| P(x) } =ext {x:A| P(x) }	[subset_squash_exteq]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } =ext {x:A| B'(x) })	[subset_sq_exteq]
Thm*  (x:A. B(x)  B'(x))  {x:A| B(x) }  {x:A| B'(x) }	[set_inc_wrt_imp_sq]
Thm*  x:A. B(x)  x  {x:A| B(x) }	[squash_to_subset]
Thm*  x:{x:A| B(x) }. B(x)	[subset_to_squash]
Thm*  P  P	[sq_sq_iff_sq]
Thm*  Dec(P)  Dec(P)	[dec_imp_dec_sq]
Thm*  (P)  P	[sq_not_iff_sq]
Thm*  P  P	[not_sq_iff_sq]

In prior sections: core rel 1 quot 1

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