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

_ :: Char
_ :: Doc
_ :: Int
_ :: [Char]
($$) :: Doc -> Doc -> Doc
(<>) :: Doc -> Doc -> Doc
nest :: Int -> Doc -> Doc
(++) :: [Char] -> [Char] -> [Char]
length :: [Char] -> Int


d1 <= d1 $$ d2
d1 <= d1 <> d2