Def   == Unit+Unit

is mentioned by

Thm*  P:(AType). (x:A. Dec(P(x)))  (!{p:(A)| x:A. p(x)  P(x) })	[dec_pred_imp_bool_decider_exists]
Thm*  (x:T. Dec(E(x)))  (f:(T). x:T. f(x)  E(x))	[dec_pred_iff_some_boolfun]
Thm*  (A Discrete)  (e:(AA). IsEqFun(A;e))	[discrete_vs_bool2]
Thm*  (A Discrete)  (e:(AA). x,y:A. (x e y)  x = y)	[discrete_vs_bool]
Thm*  {x:A| if b P(x) else Q(x) fi } Thm*  =ext Thm*  if b {x:A| P(x) } else {x:A| Q(x) } fi	[ifthenelse_distr_subtype]
Thm*  Dec(P)  (b:. b  P)	[decbl_iff_some_bool]

In prior sections: bool 1 rel 1 quot 1

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