Thms bool 1 Doc

eq_int Def i=j == if i=jtrue; false fi

Thm* i,j:. i=j

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

function_primDef x:AB(x) == PRIMITIVE {Total functions from A: x.b(x) such that b(x) B(x) for x A }

bfalse Def false ==

Thm* false

btrue Def true ==

Thm* true