I'm trying to prove the following duality theorem of fold for finite lists:

   foldr f e xs         =  foldl (flip f) e (reverse xs)

where

   reverse              :: [a] -> [a]
   reverse []           =  []
   reverse (x:xs)       =  reverse xs ++ [x]

   flip                 :: (a -> b -> c) -> b -> a -> c
   flip f y x           =  f x y

   foldr                :: (a -> b -> b) -> b -> [a] -> b
   foldr f e []         =  e
   foldr f e (x : xs)   =  f x (foldr f e xs)

   foldl                :: (b -> a -> b) -> b -> [a] -> b
   foldl f e []         =  e
   foldl f e (x : xs)   =  foldl f (f e x) xs

I'm stuck on the induction case.  Can someone help?  Here's what I've got so far:

Proof:

   Case _|_.

      Left-side reduction:

         foldr f e _|_
      =  {case exhaustion of "foldr"}
         _|_

      Right-side reduction:

         foldl (flip f) e (reverse _|_)
      =  {case exhaustion of "reverse"}
         foldl (flip f) e _|_
      =  {case exhaustion of "foldl"}
         _|_

   Case [].

      Left-side reduction:

         foldr f e []
      =  {first equation of "foldr"}
         e

      Right-side reduction:

         foldl (flip f) e (reverse [])
      =  {first equation of "reverse"}
         foldl (flip f) e []
      =  {first equation of "foldl"}
         e

   Case (x : xs).

      Left-side reduction:

         foldr f e (x : xs)
      =  {second equation of "foldr"}
         f x (foldr f e xs)
      =  {induction hypothesis: foldr f e xs = foldl (flip f) e (reverse xs)}
         f x (foldl (flip f) e (reverse xs))

      Right-side reduction:

         foldl (flip f) e (reverse (x : xs))
      =  {second equation of "reverse"}
         foldl (flip f) e (reverse xs ++ [x])

---

HotmailŪ is up to 70% faster. Now good news travels really fast. Find out more.