Prove foldl fusion law
Let me try to answer your question, I may be mistaken, so check it out first:

Let's first state the definition of foldl:

foldl :: (a -&gt; b -&gt; a) -&gt; a -&gt; [b] -&gt; a
foldl h b x = case x of 
                []     -&gt; b
                (x:xs) -&gt; foldl h (h b x) xs


Now, we aim to prove that, given f:: A -&gt; B, g:: A -&gt; C -&gt; A, h:: B -&gt; C -&gt; B, a:: A b:: B, such that:

f a = b
f (g x y) = h (f x) y, for all x, y
f is strict


Then:

f . foldl g a = foldl h b :: [C] -&gt; B


We are going to prove it by induction on the length of the list: 

Case 0:

f.foldl g a []   = foldl h b []
f (foldl g a []) = foldl h b []   -- Definition of .
f a              = b              -- Definition of foldl
True                              -- given


Case n => n+1:

let x:xs be a list of length n+1, then xs has length n, the property holds for xs. Let's check it's true for x:xs:

f (foldl g a (x:xs))   = foldl h b (x:xs)
f (foldl g (g a x) xs) = foldl h (h b x) xs  -- Definition of foldl


Now, let's take f' = f, g' = g, a' = g a x, h' = h, b' = h b x

Clearly, f' is strict, also, f' a' = b':

f' a'     = b' 
f (g a x) = h b x  -- Opening the '
h (f a) x = h b x  -- Hypothesis
h b x     = h b x  -- Hypothesis 


Now, let's check that f' (g' z y) = h' (f' z) y works for any y, z (I changed the x for a z, because we have a fixed x, the head of the list):

f' (g' z y) = h' (f' z) y
f (g z y)   = h (f z) y   -- Opening the '
                          -- OK: hypothesis


Now, since the predicate works for lists of length n, and xs has that length, and also f', g', h', a', b' make the premises true, we have that, for any list of size n, in particular xs:

f' . foldl g' a' xs      = foldl h' b' xs
f  . foldl g  (g a x) xs = foldl h (h b x) xs  -- Opening the '
f (foldl g (g a x) xs)   = foldl h (h b x) xs  -- What we were trying to reach