max expr size  =    4
  |- on ineqs  =    3
  |- on conds  =    3
max  #-tests   =  500
min  #-tests   =   25  (to consider p ==> q true)
max  #-vars    =    2  (for inequational and conditional laws)

_ :: Bool
_ :: Word2
_ :: BT Word2
_ :: [Word2]
Null :: BT Word2
insert :: Word2 -> BT Word2 -> BT Word2
delete :: Word2 -> BT Word2 -> BT Word2
isIn :: Word2 -> BT Word2 -> Bool
(<=) :: Word2 -> Word2 -> Bool
(/=) :: Word2 -> Word2 -> Bool
ordered :: [Word2] -> Bool
strictlyOrdered :: [Word2] -> Bool
toList :: BT Word2 -> [Word2]
fromList :: [Word2] -> BT Word2
isSearch :: BT Word2 -> Bool
[] :: [Word2]
True :: Bool
False :: Bool
(==) :: Bool -> Bool -> Bool
(==) :: Word2 -> Word2 -> Bool
(==) :: BT Word2 -> BT Word2 -> Bool
(==) :: [Word2] -> [Word2] -> Bool

  isIn x Null == False
   (xs == []) == (Null == fromList xs)
delete x Null == Null

         Null <= t
            t <= insert x t
   delete x t <= t
insert x Null <= insert x t

isIn x t ==> insert x t == t