Thms bool 1 Doc

nequal Def abT == a = b T

Thm* x,y:A. xy Prop

not Def A == A False

Thm* (A) Prop