feat(data/list/basic): lemmas about foldr/foldl (#3865)
This PR prepares #3864.
* Move lemmas about `foldr`/`foldl` into the appropriate section.
* Add variants of the `foldl_map`/`foldr_map` lemmas.
* Add lemmas stating that a fold over a list of injective functions is injective.
