Nuprl - Some Definitions

bfalse	`Def false ==` `Thm* false`
bool	`Def == Unit+Unit` `Thm* Type`
assert	`Def b == if b True else False fi` `Thm* b:. b Prop`
not	`Def A == A False` `Thm* (A) Prop`
ifthenelse	`Def if b t else f fi == dec(b ; t; f)` `Thm* b:, A:Type, p,q:A. if b p else q fi A`