The big_sepL_delete lemma is quite useful and is akin to big_sepM_delete.
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.