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

_ :: Bool  (holes: Bool)
_ :: Equation  (holes: Equation)
_ :: Expr  (holes: Expr)
_ :: Thyght  (holes: Thyght)
_ :: [Expr]  (holes: [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