max expr size  =    4
  |- on ineqs  =    3
  |- on conds  =    3
max  #-tests   = 6000
max  #-vars    =    2  (for inequational and conditional laws)

_ :: Bool
_ :: Equation
_ :: Expr
_ :: Thyght
_ :: [Expr]
okThy :: Thyght -> Bool
insert :: Expr -> Thyght -> Thyght
complete :: Thyght -> Thyght
normalize :: Thyght -> Expr -> Expr
equivalent :: Thyght -> Expr -> Expr -> Bool
append :: Thyght -> [Expr] -> Thyght
emptyThy :: Thyght
True :: Bool
False :: Bool
Equation :: Expr -> Expr -> Equation

              okThy t == True
     equivalent t e e == True
     equivalent t e f == equivalent t f e
 normalize emptyThy e == e
complete (complete t) == complete t