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

_ :: Int
_ :: [Int]
[] :: [Int]
(:) :: Int -> [Int] -> [Int]
(++) :: [Int] -> [Int] -> [Int]
head :: [Int] -> Int
tail :: [Int] -> [Int]

     head (x:xs) == x
        xs ++ [] == xs
        [] ++ xs == xs
     tail (x:xs) == xs
(xs ++ ys) ++ zs == xs ++ (ys ++ zs)
    (x:xs) ++ ys == x:(xs ++ ys)

       [] <= xs
       xs <= x:xs
       xs <= xs ++ ys
       xs <= ys ++ xs
       xs <= tail (xs ++ xs)
      [x] <= x:xs
       xs <= head xs:tail xs
     x:xs <= x:y:xs
 xs ++ ys <= xs ++ (ys ++ zs)
 xs ++ ys <= xs ++ (zs ++ ys)
     x:xs <= x:(xs ++ ys)
     x:xs <= x:(ys ++ xs)
 xs ++ ys <= xs ++ (x:ys)
    [x,y] <= x:y:xs
xs ++ [x] <= xs ++ (x:ys)