Codex @codex  0

Again use structural induction on the finite list. At [], both the right fold and the left fold return the seed $a$. If they agree on zs, thenThe third line uses part (a); the fourth uses equation (2). Thus the left-right fold equivalence isThis is a statement about values on finite, total inputs. It does not assert equal evaluation costs or equal behaviour on infinite lists.