diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index cf004a0658b47f49a90c7b29c4879e5c4ba5df6f..91cc46333ad5aaf6514730075116307d5c2cf680 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -97,6 +97,9 @@ Section list.
     revert f. induction l1 as [|x l1 IH]=> f /=; first by rewrite left_id.
     by rewrite IH assoc.
   Qed.
+  Lemma big_opL_snoc f l x :
+    ([^o list] k↦y ∈ l ++ [x], f k y) ≡ ([^o list] k↦y ∈ l, f k y) `o` f (length l) x.
+  Proof. rewrite big_opL_app big_opL_singleton Nat.add_0_r //. Qed.
 
   Lemma big_opL_unit l : ([^o list] k↦y ∈ l, monoid_unit) ≡ (monoid_unit : M).
   Proof. induction l; rewrite /= ?left_id //. Qed.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 70f4253340f3ff4f759cfbd78517182ebaa01134..69ef212c14947f4017ea48f4af2c6de7a86a559e 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -91,6 +91,9 @@ Section sep_list.
     ([∗ list] k↦y ∈ l1 ++ l2, Φ k y)
     ⊣⊢ ([∗ list] k↦y ∈ l1, Φ k y) ∗ ([∗ list] k↦y ∈ l2, Φ (length l1 + k) y).
   Proof. by rewrite big_opL_app. Qed.
+  Lemma big_sepL_snoc Φ l x :
+    ([∗ list] k↦y ∈ l ++ [x], Φ k y) ⊣⊢ ([∗ list] k↦y ∈ l, Φ k y) ∗ Φ (length l) x.
+  Proof. by rewrite big_opL_snoc. Qed.
 
   Lemma big_sepL_submseteq `{BiAffine PROP} (Φ : A → PROP) l1 l2 :
     l1 ⊆+ l2 → ([∗ list] y ∈ l2, Φ y) ⊢ [∗ list] y ∈ l1, Φ y.
@@ -423,6 +426,24 @@ Section sep_list2.
     - by rewrite -assoc IH.
   Qed.
 
+  Lemma big_sepL2_snoc Φ x1 x2 l1 l2 :
+    ([∗ list] k↦y1;y2 ∈ (l1 ++ [x1]);(l2 ++ [x2]), Φ k y1 y2) ⊣⊢
+    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ∗ Φ (length l1) x1 x2.
+  Proof.
+    apply (anti_symm (⊢)); last first.
+    - apply wand_elim_l'. rewrite big_sepL2_app. apply wand_mono; last done.
+      rewrite big_sepL2_singleton Nat.add_0_r. done.
+    - rewrite big_sepL2_app_inv_l. apply exist_elim=>l2l. apply exist_elim=>l2r.
+      apply pure_elim_l=>Hl2.
+      apply (pure_elim (length [x1] = length l2r)).
+      { rewrite !big_sepL2_length sep_elim_r. done. }
+      simpl. destruct l2r as [? l2r|]; first done.
+      destruct l2r as [|]; last done. intros _.
+      apply app_inj_tail in Hl2 as [-> ->].
+      apply sep_mono_r.
+      rewrite big_sepL2_singleton Nat.add_0_r. done.
+  Qed.
+
   (** The lemmas [big_sepL2_mono], [big_sepL2_ne] and [big_sepL2_proper] are more
   generic than the instances as they also give [li !! k = Some yi] in the premise. *)
   Lemma big_sepL2_mono Φ Ψ l1 l2 :