Thms bool 1 Doc

nequal Def abT == a = b T

Thm* x,y:A. xy Prop

bfalse Def false ==

Thm* false

btrue Def true ==

Thm* true

bool Def == Unit+Unit

Thm* Type

not Def A == A False

Thm* (A) Prop