Generalise fold-fusion results

[gallais]

Cf. this blog post by @oisdk

We’re not using the proofs in Agda’s standard library because these are tied to propositional equality. In other words, instead of using an abstract binary relation, they prove things over actual equality. That’s all well and good, but as you can see above, we don’t need propositional equality: we don’t even need the relation to be an equivalence, we just need transitivity and reflexivity.

[jamesmckinna]

Well, we now (PR #1668) have some more systematic ≡-based fold*-fusion results in Data.Vec.Properties (and soon, some more heterogeneous ones about reverse to go... somewhere), so part of that reconsideration might be to generalise these things.

One day.