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

_ :: Int
_ :: [Int]
[] :: [Int]
(:) :: Int -> [Int] -> [Int]
(++) :: [Int] -> [Int] -> [Int]
0 :: Int
length :: [Int] -> Int

    length (x:xs) == length (y:xs)
length (xs ++ ys) == length (ys ++ xs)

         0 <= length xs
 length xs <= length (x:xs)
 length xs <= length (xs ++ ys)
length [x] <= length (x:xs)