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 Fixed by Robbert's changes.
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.