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 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.
Edited by Isaac van Bakel