I am reading Software Foundations, chapter Logic. See here. There is an informal exercise that asks:

Are there any important properties of the function

`forallb`

which are not captured by this specification?

Here are the relevant types:

```
forallb: (?X -> bool) -> list ?X -> bool
All: (?T -> Prop) -> list ?T -> Prop
forallb_true_iff: forall (X : Type) (test : X -> bool) (l : list X),
forallb' test l = true <-> All (fun x : X => test x = true) l
```

I have proven this theorem with two variants of `forallb`

that process the list in either usual or reverse order. So, the order of evaluation is not captured.

- Is this the
*«important property»*the book hints at? - How hard would it be to formally prove that
`forallb_true_iff`

nails`forallb`

exactly up to the order of evaluation?