Add lemmas for commuting funcs with folds

These lemmas were helpful to me in recent proofs (in particular, the multiset one is used for iris/iris#923.) They allow for moving a unitary function on a fold accumulator in and out of the fold as necessary, provided the function commutes appropriately with the fold function.

The location of the multiset lemma in the file is not ideal, since it has to come after gmultiset_ind, which is well after all the other fold lemmas. However, proving it without gmultiset_ind is much harder, and moving gmultiset_ind further up the file is itself non-trivial, so I've opted not to try. Fixed by Robbert's changes.