Def   == Unit+Unit

is mentioned by

Thm*  p:(a). {x:a| p(x) } ~ (size(a)(p))	[card_st_vs_boolsize]
Thm*  a:. size(a)  (a)	[boolsize_wf]
Thm*  e:(BB).  Thm*  IsEqFun(B;e) Thm*   Thm*  (a:, f:(a onto B). (y.least x:. (f(x)) e y)  B inj a)	[nsub_surj_imp_a_rev_inj_gen]
Thm*   ~ 2	[nsub_bool]
Thm*  {x:A| if b P(x) else Q(x) fi } ~ if b {x:A| P(x) } else {x:A| Q(x) } fi	[ifthenelse_distr_subtype_ooc]
Thm*  e:(BB).  Thm*  IsEqFun(B;e)  (a:, f:(a onto B), y:B. f(least x:. (f(x)) e y) = y)	[nsub_surj_least_preimage_works_gen]
Thm*  e:(BB).  Thm*  IsEqFun(B;e)  (a:, f:(a onto B), y:B. (least x:. (f(x)) e y)  a)	[nsub_surj_least_preimage_total_gen]
Thm*  p:{p:()| i:. p(i) }. p(least i:. p(i))	[least_satisfies2]
Thm*  p:{p:()| i:. p(i) }, j:(least i:. p(i)). p(j)	[least_is_least2]
Thm*  k:, p:{p:(k)| i:k. p(i) }, j:(least i:. p(i)). p(j)	[least_is_least]
Thm*  k:, p:{p:(k)| i:k. p(i) }. p(least i:. p(i))	[least_satisfies]
Thm*  p:{p:()| i:. p(i) }. (least i:. p(i))	[least_wf2]
Thm*  p:{p:()| i:. p(i) }.  Thm*  (least i:. p(i))  {i:| p(i) & (j:. j<i  p(j)) }	[least_characterized2]
Thm*  k:, p:{p:(k)| i:k. p(i) }. (least i:. p(i))  k	[least_wf]
Thm*  k:, p:{p:(k)| i:k. p(i) }. Thm*  (least i:. p(i))  {i:k| p(i) & (j:i. p(j)) }	[least_characterized]
Thm*  A,X:Type, P:(A), y:A, f:(XA). Thm*  (Replace values x s.t. P(x) by y in f)  XA	[replace_fn_values_wf]
Def  a {k}  == {p:(a)| size(a)(p) = k }	[sized_bool]

In prior sections: bool 1 rel 1 quot 1 LogicSupplement SimpleMulFacts

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