diff --git a/CHANGELOG.md b/CHANGELOG.md
index f7a79c72b0bfda539f125b660160d7fb8298141d..d0f2c9485fe0b5acb3332dca1a5d12506e398a63 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -81,6 +81,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
   and either affine or absorbing.
 * Fix the statement of the lemma `fupd_plainly_laterN`; the old lemma was a
   duplicate of `fupd_plain_laterN`.
+* Strengthen `big_sepL2_app_inv` by weakening a premise (it is sufficient for
+  one of the two pairs of lists to have equal length).
 
 **Changes in `proofmode`:**
 
diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index cf004a0658b47f49a90c7b29c4879e5c4ba5df6f..1c6aafe2c7c7ef87c7951f73a9a40c29abbb4316 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.
@@ -214,6 +217,26 @@ Proof.
   revert f. induction l as [|x l IH]=> f; csimpl=> //. by rewrite big_opL_app IH.
 Qed.
 
+Lemma big_opL_sep_zip_with {A B C} (f : A → B → C) (g1 : C → A) (g2 : C → B)
+    (h1 : nat → A → M) (h2 : nat → B → M) l1 l2 :
+  (∀ x y, g1 (f x y) = x) →
+  (∀ x y, g2 (f x y) = y) →
+  length l1 = length l2 →
+  ([^o list] k↦xy ∈ zip_with f l1 l2, h1 k (g1 xy) `o` h2 k (g2 xy)) ≡
+  ([^o list] k↦x ∈ l1, h1 k x) `o` ([^o list] k↦y ∈ l2, h2 k y).
+Proof.
+  intros Hlen Hg1 Hg2. rewrite big_opL_op.
+  rewrite -(big_opL_fmap g1) -(big_opL_fmap g2).
+  rewrite fmap_zip_with_r; [|auto with lia..].
+  by rewrite fmap_zip_with_l; [|auto with lia..].
+Qed.
+
+Lemma big_opL_sep_zip {A B} (h1 : nat → A → M) (h2 : nat → B → M) l1 l2 :
+  length l1 = length l2 →
+  ([^o list] k↦xy ∈ zip l1 l2, h1 k xy.1 `o` h2 k xy.2) ≡
+  ([^o list] k↦x ∈ l1, h1 k x) `o` ([^o list] k↦y ∈ l2, h2 k y).
+Proof. by apply big_opL_sep_zip_with. Qed.
+
 (** ** Big ops over finite maps *)
 
 Lemma big_opM_empty `{Countable K} {B} (f : K → B → M) :
@@ -394,6 +417,29 @@ Section gmap.
   Qed.
 End gmap.
 
+Lemma big_opM_sep_zip_with `{Countable K} {A B C}
+    (f : A → B → C) (g1 : C → A) (g2 : C → B)
+    (h1 : K → A → M) (h2 : K → B → M) m1 m2 :
+  (∀ x y, g1 (f x y) = x) →
+  (∀ x y, g2 (f x y) = y) →
+  (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
+  ([^o map] k↦xy ∈ map_zip_with f m1 m2, h1 k (g1 xy) `o` h2 k (g2 xy)) ≡
+  ([^o map] k↦x ∈ m1, h1 k x) `o` ([^o map] k↦y ∈ m2, h2 k y).
+Proof.
+  intros Hdom Hg1 Hg2. rewrite big_opM_op.
+  rewrite -(big_opM_fmap g1) -(big_opM_fmap g2).
+  rewrite map_fmap_zip_with_r; [|naive_solver..].
+  by rewrite map_fmap_zip_with_l; [|naive_solver..].
+Qed.
+
+Lemma big_opM_sep_zip `{Countable K} {A B}
+    (h1 : K → A → M) (h2 : K → B → M) m1 m2 :
+  (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
+  ([^o map] k↦xy ∈ map_zip m1 m2, h1 k xy.1 `o` h2 k xy.2) ≡
+  ([^o map] k↦x ∈ m1, h1 k x) `o` ([^o map] k↦y ∈ m2, h2 k y).
+Proof. intros. by apply big_opM_sep_zip_with. Qed.
+
+
 (** ** Big ops over finite sets *)
 Section gset.
   Context `{Countable A}.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 6edadcd3027f4c58642fc0d8d38997962bb88a8d..44a785eec52b34a9b032b63f00df72af634e19b0 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.
@@ -291,25 +294,35 @@ Section sep_list.
   Proof. induction 1; simpl; apply _. Qed.
 End sep_list.
 
-Section sep_list_more.
-  Context {A : Type}.
-  Implicit Types l : list A.
-  Implicit Types Φ Ψ : nat → A → PROP.
-  (* Some lemmas depend on the generalized versions of the above ones. *)
-
-  Lemma big_sepL_zip_with {B C} Φ f (l1 : list B) (l2 : list C) :
-    ([∗ list] k↦x ∈ zip_with f l1 l2, Φ k x)
-    ⊣⊢ ([∗ list] k↦x ∈ l1, if l2 !! k is Some y then Φ k (f x y) else emp).
-  Proof.
-    revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //=.
-    - by rewrite big_sepL_emp left_id.
-    - by rewrite IH.
-  Qed.
-End sep_list_more.
+(* Some lemmas depend on the generalized versions of the above ones. *)
+Lemma big_sepL_sep_zip_with {A B C} (f : A → B → C) (g1 : C → A) (g2 : C → B)
+    (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
+  (∀ x y, g1 (f x y) = x) →
+  (∀ x y, g2 (f x y) = y) →
+  length l1 = length l2 →
+  ([∗ list] k↦xy ∈ zip_with f l1 l2, Φ1 k (g1 xy) ∗ Φ2 k (g2 xy)) ⊣⊢
+  ([∗ list] k↦x ∈ l1, Φ1 k x) ∗ ([∗ list] k↦y ∈ l2, Φ2 k y).
+Proof. apply big_opL_sep_zip_with. Qed.
+
+Lemma big_sepL_sep_zip {A B} (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
+  length l1 = length l2 →
+  ([∗ list] k↦xy ∈ zip l1 l2, Φ1 k xy.1 ∗ Φ2 k xy.2) ⊣⊢
+  ([∗ list] k↦x ∈ l1, Φ1 k x) ∗ ([∗ list] k↦y ∈ l2, Φ2 k y).
+Proof. apply big_opL_sep_zip. Qed.
+
+Lemma big_sepL_zip_with {A B C} (Φ : nat → A → PROP) f (l1 : list B) (l2 : list C) :
+  ([∗ list] k↦x ∈ zip_with f l1 l2, Φ k x) ⊣⊢
+  ([∗ list] k↦x ∈ l1, if l2 !! k is Some y then Φ k (f x y) else emp).
+Proof.
+  revert Φ l2; induction l1 as [|x l1 IH]=> Φ [|y l2] //=.
+  - by rewrite big_sepL_emp left_id.
+  - by rewrite IH.
+Qed.
 
+(** ** Big ops over two lists *)
 Lemma big_sepL2_alt {A B} (Φ : nat → A → B → PROP) l1 l2 :
-  ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2)
-  ⊣⊢ ⌜ length l1 = length l2 ⌝ ∧ [∗ list] k ↦ y ∈ zip l1 l2, Φ k (y.1) (y.2).
+  ([∗ list] k↦y1;y2 ∈ l1; l2, Φ k y1 y2) ⊣⊢
+  ⌜ length l1 = length l2 ⌝ ∧ [∗ list] k ↦ xy ∈ zip l1 l2, Φ k (xy.1) (xy.2).
 Proof.
   apply (anti_symm _).
   - apply and_intro.
@@ -323,7 +336,6 @@ Proof.
     induction Hl as [|x1 l1 x2 l2 _ _ IH]=> Φ //=. by rewrite -IH.
 Qed.
 
-(** ** Big ops over two lists *)
 Section sep_list2.
   Context {A B : Type}.
   Implicit Types Φ Ψ : nat → A → B → PROP.
@@ -404,14 +416,36 @@ Section sep_list2.
     by rewrite IH -assoc.
   Qed.
   Lemma big_sepL2_app_inv Φ l1 l2 l1' l2' :
-    length l1 = length l1' →
+    length l1 = length l1' ∨ length l2 = length l2' →
     ([∗ list] k↦y1;y2 ∈ l1 ++ l2; l1' ++ l2', Φ k y1 y2) -∗
     ([∗ list] k↦y1;y2 ∈ l1; l1', Φ k y1 y2) ∗
     ([∗ list] k↦y1;y2 ∈ l2; l2', Φ (length l1 + k)%nat y1 y2).
   Proof.
-    revert Φ l1'. induction l1 as [|x1 l1 IH]=> Φ -[|x1' l1'] //= ?; simplify_eq.
+    revert Φ l1'. induction l1 as [|x1 l1 IH]=> Φ -[|x1' l1'] /= Hlen.
     - by rewrite left_id.
-    - by rewrite -assoc IH.
+    - destruct Hlen as [[=]|Hlen]. rewrite big_sepL2_length Hlen /= app_length.
+      apply pure_elim'; lia.
+    - destruct Hlen as [[=]|Hlen]. rewrite big_sepL2_length -Hlen /= app_length.
+      apply pure_elim'; lia.
+    - by rewrite -assoc IH; last lia.
+  Qed.
+  Lemma big_sepL2_app_same_length Φ l1 l2 l1' l2' :
+    length l1 = length l1' ∨ length l2 = length l2' →
+    ([∗ list] k↦y1;y2 ∈ l1 ++ l2; l1' ++ l2', Φ k y1 y2) ⊣⊢
+    ([∗ list] k↦y1;y2 ∈ l1; l1', Φ k y1 y2) ∗
+    ([∗ list] k↦y1;y2 ∈ l2; l2', Φ (length l1 + k)%nat y1 y2).
+  Proof.
+    intros. apply (anti_symm _).
+    - by apply big_sepL2_app_inv.
+    - apply wand_elim_l'. apply big_sepL2_app.
+  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.
+    rewrite big_sepL2_app_same_length; last by auto.
+    by rewrite big_sepL2_singleton Nat.add_0_r.
   Qed.
 
   (** The lemmas [big_sepL2_mono], [big_sepL2_ne] and [big_sepL2_proper] are more
@@ -619,6 +653,20 @@ Section sep_list2.
     by rewrite IH.
   Qed.
 
+  Lemma big_sepL_sepL2 (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
+    length l1 = length l2 →
+    ([∗ list] k↦y1;y2 ∈ l1;l2, Φ1 k y1 ∗ Φ2 k y2) ⊣⊢
+    ([∗ list] k↦y1 ∈ l1, Φ1 k y1) ∗ ([∗ list] k↦y2 ∈ l2, Φ2 k y2).
+  Proof.
+    intros. rewrite -big_sepL_sep_zip // big_sepL2_alt pure_True // left_id //.
+  Qed.
+  Lemma big_sepL_sepL2_2 (Φ1 : nat → A → PROP) (Φ2 : nat → B → PROP) l1 l2 :
+    length l1 = length l2 →
+    ([∗ list] k↦y1 ∈ l1, Φ1 k y1) -∗
+    ([∗ list] k↦y2 ∈ l2, Φ2 k y2) -∗
+    [∗ list] k↦y1;y2 ∈ l1;l2, Φ1 k y1 ∗ Φ2 k y2.
+  Proof. intros. apply wand_intro_r. by rewrite big_sepL_sepL2. Qed.
+
   Global Instance big_sepL2_nil_persistent Φ :
     Persistent ([∗ list] k↦y1;y2 ∈ []; [], Φ k y1 y2).
   Proof. simpl; apply _. Qed.
@@ -644,6 +692,14 @@ Section sep_list2.
   Proof. rewrite big_sepL2_alt. apply _. Qed.
 End sep_list2.
 
+Lemma big_sepL_sepL2_diag {A} (Φ : nat → A → A → PROP) (l : list A) :
+  ([∗ list] k↦y ∈ l, Φ k y y) -∗
+  ([∗ list] k↦y1;y2 ∈ l;l, Φ k y1 y2).
+Proof.
+  rewrite big_sepL2_alt. rewrite pure_True // left_id.
+  rewrite zip_diag big_sepL_fmap /=. done.
+Qed.
+
 Lemma big_sepL2_ne_2 {A B : ofe}
     (Φ Ψ : nat → A → B → PROP) l1 l2 l1' l2' n :
   l1 ≡{n}≡ l1' → l2 ≡{n}≡ l2' →
@@ -1109,7 +1165,31 @@ Section map.
   Proof. rewrite big_opM_eq. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
 End map.
 
+(* Some lemmas depend on the generalized versions of the above ones. *)
+Lemma big_sepM_sep_zip_with `{Countable K} {A B C}
+    (f : A → B → C) (g1 : C → A) (g2 : C → B)
+    (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) m1 m2 :
+  (∀ x y, g1 (f x y) = x) →
+  (∀ x y, g2 (f x y) = y) →
+  (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
+  ([∗ map] k↦xy ∈ map_zip_with f m1 m2, Φ1 k (g1 xy) ∗ Φ2 k (g2 xy)) ⊣⊢
+  ([∗ map] k↦x ∈ m1, Φ1 k x) ∗ ([∗ map] k↦y ∈ m2, Φ2 k y).
+Proof. apply big_opM_sep_zip_with. Qed.
+
+Lemma big_sepM_sep_zip `{Countable K} {A B}
+    (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) m1 m2 :
+  (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
+  ([∗ map] k↦xy ∈ map_zip m1 m2, Φ1 k xy.1 ∗ Φ2 k xy.2) ⊣⊢
+  ([∗ map] k↦x ∈ m1, Φ1 k x) ∗ ([∗ map] k↦y ∈ m2, Φ2 k y).
+Proof. apply big_opM_sep_zip. Qed.
+
 (** ** Big ops over two maps *)
+Lemma big_sepM2_alt `{Countable K} {A B} (Φ : K → A → B → PROP) m1 m2 :
+  ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) ⊣⊢
+  ⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌝ ∧
+  [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2.
+Proof. by rewrite big_sepM2_eq. Qed.
+
 Section map2.
   Context `{Countable K} {A B : Type}.
   Implicit Types Φ Ψ : K → A → B → PROP.
@@ -1474,6 +1554,20 @@ Section map2.
     apply big_sepM2_mono. eauto.
   Qed.
 
+  Lemma big_sepM_sepM2 (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) m1 m2 :
+    (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
+    ([∗ map] k↦y1;y2 ∈ m1;m2, Φ1 k y1 ∗ Φ2 k y2) ⊣⊢
+    ([∗ map] k↦y1 ∈ m1, Φ1 k y1) ∗ ([∗ map] k↦y2 ∈ m2, Φ2 k y2).
+  Proof.
+    intros. rewrite -big_sepM_sep_zip // big_sepM2_alt pure_True // left_id //.
+  Qed.
+  Lemma big_sepM_sepM2_2 (Φ1 : K → A → PROP) (Φ2 : K → B → PROP) m1 m2 :
+    (∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k)) →
+    ([∗ map] k↦y1 ∈ m1, Φ1 k y1) -∗
+    ([∗ map] k↦y2 ∈ m2, Φ2 k y2) -∗
+    [∗ map] k↦y1;y2 ∈ m1;m2, Φ1 k y1 ∗ Φ2 k y2.
+  Proof. intros. apply wand_intro_r. by rewrite big_sepM_sepM2. Qed.
+
   Global Instance big_sepM2_empty_persistent Φ :
     Persistent ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2).
   Proof. rewrite big_sepM2_empty. apply _. Qed.
@@ -1499,6 +1593,14 @@ Section map2.
   Proof. intros. rewrite big_sepM2_eq /big_sepM2_def. apply _. Qed.
 End map2.
 
+Lemma big_sepM_sepM2_diag `{Countable K} {A} (Φ : K → A → A → PROP) (m : gmap K A) :
+  ([∗ map] k↦y ∈ m, Φ k y y) -∗
+  ([∗ map] k↦y1;y2 ∈ m;m, Φ k y1 y2).
+Proof.
+  rewrite big_sepM2_alt. rewrite pure_True; last naive_solver. rewrite left_id.
+  rewrite map_zip_diag big_sepM_fmap. done.
+Qed.
+
 Lemma big_sepM2_ne_2 `{Countable K} (A B : ofe)
     (Φ Ψ : K → A → B → PROP) m1 m2 m1' m2' n :
   m1 ≡{n}≡ m1' → m2 ≡{n}≡ m2' →