max expr size  =    4
  |- on conds  =    3
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
 xs <= x:xs
 xs <= xs ++ ys
 xs <= ys ++ xs
 xs <= tail (xs ++ xs)
[x] <= x:xs