Implement `big_sepL_delete`

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.

mentioned in commit 3bc1f853

Thanks for the MR.

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.

Done, see 3bc1f853, thus closing this MR.

closed