Def  T == {:True| T }

is mentioned by

Thm*  (x:A. Dec(P(x)))  (A ~ ({x:A| P(x) }+{x:A| P(x) }))	[card_split_decbl_squash]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } ~ {x:A| B'(x) })	[set_functionality_wrt_one_one_corr_n_pred]
Thm*  Bij(A; A'; f) Thm*   Thm*  (x:A. B(x)  B'(f(x)))  ({x:A| B(x) } ~ {x:A'| B'(x) })	[card_settype_sq]
Thm*  {x:A| B(x) } ~ {x:A| B(x) }	[subset_sq_remove_card]

In prior sections: core rel 1 quot 1 LogicSupplement

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