+Or rather, it should give us a list' version of that, which takes a function `k` and value `z` as arguments, and returns the right fold of `k` and `z` over those elements. What does our formula
+
+ fun k z -> u (fun a b -> f a k b) z
+
+do? Well, for each element `a` in `u`, it applies `f` to that `a`, getting one of the lists:
+
+ []
+ [2]
+ [2; 4]
+ [2; 4; 8]
+
+(or rather, their list' versions). Then it takes the accumulated result `b` of previous steps in the fold, and it folds `k` and `b` over the list generated by `f a`. The result of doing so is passed on to the next step as the accumulated result so far.
+
+So if, for example, we let `k` be `+` and `z` be `0`, then the computation would proceed:
+
+ 0 ==>
+ right-fold + and 0 over [2; 4; 8] = 2+4+8+0 ==>
+ right-fold + and 2+4+8+0 over [2; 4] = 2+4+2+4+8+0 ==>
+ right-fold + and 2+4+2+4+8+0 over [2] = 2+2+4+2+4+8+0 ==>
+ right-fold + and 2+2+4+2+4+8+0 over [] = 2+2+4+2+4+8+0
+
+which indeed is the result of right-folding + and 0 over `[2; 2; 4; 2; 4; 8]`. If you trace through how this works, you should be able to persuade yourself that our formula:
+
+ fun k z -> u (fun a b -> f a k b) z
+
+will deliver just the same folds, for arbitrary choices of `k` and `z` (with the right types), and arbitrary list's `u` and appropriately-typed `f`s, as
+
+ fun k z -> List.fold_right k (concat (map f u)) z
+
+would.
+
+For future reference, we might make two eta-reductions to our formula, so that we have instead:
+
+ let l'_bind = fun k -> u (fun a -> f a k);;
+
+Let's make some more tests: