big_sepL_delete lemma is quite useful and is akin to
Lemma big_sepL_delete Φ l i x : l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊣⊢ Φ i x ∗ [∗ list] k↦y ∈ l, ⌜ k ≠ i ⌝ → Φ k y.
I use it when
big_sepL_lookup_acc is not enough, ie when I need to have access to the rest of the list as well.
I don't think that it can be implemented on the level of monoids, because it relies on the fact that we have this ⌜ k ≠ i ⌝ assumption. Furthermore, I was not able to come up with a shorter proof. If anyone knows how to compresses the two parts of the proof into one, I'd really appreciate that.