Def  b == if b True else False fi

is mentioned by

Thm*  p:(a {k} ). {i:a| p(i) } ~ k	[card_st_sized_bool]
Thm*  p:(a). {x:a| p(x) } ~ (size(a)(p))	[card_st_vs_boolsize]
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]

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

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