Proving equality between foldl recursive and iterative fold Hi I have two definitions of fold. I will call them foldl which is recursive and fold$_{itr}$ which is iterative. 

I am looking for an algebraic proof that the two definitions are equal ideally through structural induction.

Definition for foldl

foldl(c,h) nil = c

foldl(c, h) (list, element) = h (foldl (c, h) list, element)


Definition for fold$_{itr}$ 

fold$_{itr}$ (c, h) nil = nil

fold$_{itr}$ (c, h) (element, list) = fold$_{itr}$ (h(c, element), h) list
The two definitions are not equal. Consider $h$ defined by
\begin{align*}
h(c, a) = 10 \cdot c + a
\end{align*}
and $c = 0$. Then
$$\mathsf{foldl} \, (c,h) \, [1,2,3] = 321$$
but
$$\mathsf{fold}_{itr} \, (c,h) \, [1,2,3] = 123.$$