content: {-@ LIQUID "--reflection" @-}
  {-@ LIQUID "--ple"        @-}
  
  module Lists where
  
  import Language.Haskell.Liquid.ProofCombinators
  import Prelude hiding (length, (++))
  
  {-@ infixr ++ @-}
  
  
  {-@ propConst1 :: () -> { (((C 1 Emp) ++ Emp) ++ Emp) == (C 1 Emp) } @-}
  propConst1 :: () -> Proof
  propConst1 _ = trivial 
  
  
  {-@ automatic-instances propConst2 @-}
  {-@ propConst2 :: () -> { (((C 1 (C 2 Emp)) ++ Emp) ++ Emp) == (C 1 (C 2 Emp)) } @-}
  propConst2 :: () -> Proof
  propConst2 _ = trivial 
  
  
  {-@ automatic-instances propConst3 @-}
  {-@ propConst3 :: () -> { (((C 1 (C 2 (C 3 Emp))) ++ Emp) ++ Emp) == (C 1 (C 2 (C 3 Emp))) } @-}
  propConst3 :: () -> Proof
  propConst3 _ = trivial 
  
  
  prop :: a -> L a -> L a -> L a -> Proof 
  {-@ prop :: x:a -> xs:L a -> ys:L a -> zs:L a 
           -> {((C x xs) ++ ys) ++ zs == C x ((xs ++ ys) ++ zs) } @-} 
  prop x xs ys zs = trivial
  
  
  
  data L a = Emp | C a (L a)
  {-@ data L [length] a = Emp | C {x::a, xs :: L a } @-}
  
  {-@ measure length @-}
  length :: L a -> Int
  {-@ length :: L a -> Nat @-}
  length Emp        = 0
  length (C _ xs) = 1 + length xs
  
  {-@ axiomatize ++ @-}
  (++) :: L a -> L a -> L a
  Emp      ++ ys = ys
  (C x xs) ++ ys = C x (xs ++ ys)
  