assert	Def b == if b True else False fi Thm* b:. b 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
bool	Def == Unit+Unit Thm* Type