Short proof of `big_sepL_delete`.

This is a substitute for !136.

theories/base_logic/big_op.v

@@ -149,6 +149,19 @@ Section list.
     by rewrite persistently_impl_wand persistently_elim wand_elim_l.
   Qed.
 
+  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.
+  Proof.
+    intros. rewrite -(take_drop_middle l i x) // !big_sepL_app /= Nat.add_0_r.
+    rewrite take_length_le; last eauto using lookup_lt_Some, Nat.lt_le_incl.
+    rewrite pure_False; last by intros []. rewrite False_impl left_id.
+    rewrite assoc -!(comm _ (Φ _ _)) -assoc. do 2 f_equiv.
+    - apply big_sepL_proper=> k y Hk. apply lookup_lt_Some in Hk.
+      rewrite take_length in Hk. by rewrite pure_True ?True_impl; last lia.
+    - apply big_sepL_proper=> k y _. by rewrite pure_True ?True_impl; last lia.
+  Qed.
+
   Global Instance big_sepL_nil_plain Φ : Plain ([∗ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.
   Global Instance big_sepL_plain Φ l :