content: \begin{code}
  module SortedLists where
  \end{code}
  
  I want to prove that in a sorted list every element is `>=` than the head:
  
  \begin{code}
  {-@ type SL a = [a]<{\x v -> x <= v}> @-}
  
  {-@ measure head :: [a] -> a
      head (x:xs) = x
    @-}
  \end{code}
  
  
  Turns out that to prove it I have to compose the list using `:`
  (liquidHaskell only proves `proveOK`)
  \begin{code}
  {-@ propOKA, propOKB, propBADA, propBADB, propBADC :: 
        Ord a => xs:(SL a)  -> [{v:a|v >= (head xs)}] 
    @-}
  propOKA, propOKB, propBADA, propBADB, propBADC :: 
        Ord a => [a] -> [a]
  \end{code}
  
  \begin{code}
  propOKA xxs@(x:xs) = x:xs
  propOKB xxs@(x:xs) = listID xxs
  
  listID (x:xs) = (x:xs)
  listID []     = []
  \end{code}
  
  We know that both `x` and `xs` satisfy the desired property 
  but polymorphism on `:` is the way to transfer this information to the result.
  Any attempt that doesn't use this information fails:
  \begin{code}
  propBADA xxs@(x:xs) = xxs
  propBADB xxs@(x:xs) = id xxs
  propBADC xxs@(x:xs) = listID' xxs
  
  {-@ listID' :: forall <p :: a -> a -> Prop> . [a]<p> -> [a]<p> @-}
  listID' :: [a] -> [a]
  listID' (x:xs) = (x:xs)
  listID' []     = []
  \end{code}
  
  So, the following version of `merge` fails:
  
  \begin{code}
  {-@ LIQUID "--no-termination" @-}
  {-@ merge :: Ord a => (SL a) -> (SL a) -> (SL a) @-}
  merge :: Ord a => [a] -> [a] -> [a]
  merge xxs@(x:xs) yys@(y:ys)
    | x <= y    = x : merge xs yys
    | otherwise = y : merge xxs ys
  \end{code}
  
  