Add lemmas for creating big op from duplicable resource

Currently, there is no way to change or inject a duplicable resource into a big op. This MR adds lemmas for doing that.

In my use case, I combine this lemma with big_sepS_sep and big_sepS_impl to change the proposition in a big op using a duplicable resource.

I didn't add a big_sepM2_dupl as that didn't seem useful given that the proposition doesn't use the keys or values.

I'm not sure about the name. dupl is short for duplicable and that seems reasonable. But, the term duplicable isn't used anywhere else in the Coq code.