 Left-fold fusion law

If $f$ is a strict function and $f(g(a,x))=h(f(a),x)$ for every $a,x$, then f (foldl g a xs) = foldl h (f a) xs. Prove the equation simultaneously for all accumulators by structural induction on the list. The empty case is immediate; at a cons, apply the hypothesis with accumulator g a x and then rewrite its image using the assumed equation. At the bottom value, strictness supplies the required equality. For pure definable functions, equality on finite partial lists extends to infinite lazy lists by finite approximations. For finite terminating spines alone, strictness is unnecessary.