Thms bool 1 Doc

eq_atom Def x=yAtom == if x=yAtomtrue; false fi

Thm* x,y:Atom. x=yAtom

bfalse Def false ==

Thm* false

btrue Def true ==

Thm* true