Thms bool 1 Doc

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

Thm* i,j:. i=j

btrue Def true ==

Thm* true

bool Def == Unit+Unit

Thm* Type

not Def A == A False

Thm* (A) Prop

bfalse Def false ==

Thm* false