Nuprl - Some Definitions

bor	`Def p q == if p true else q fi` `Thm* p,q:. (p q)`
btrue	`Def true ==` `Thm* true`
bool	`Def == Unit+Unit` `Thm* Type`
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`