diff --git a/CHANGELOG.md b/CHANGELOG.md
index 25e3b0cd50efb805ec177dc49d7306cc0a9e5f1e..0399e0d88846ed54c2db3e1e33c52b40b297a1ab 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -51,6 +51,8 @@ Coq 8.8 and 8.9 are no longer supported.
   versions of the lemmas for the specific cases.
 - Rename `_11` and `_12` into `_1_1` and `_1_2`, respectively. These suffixes
   are used for `A → B1` and `A → B2` variants of `A ↔ B1 ∧ B2` lemmas.
+- Rename `Forall_Forall2` → `Forall_Forall2_diag` to be consistent with the
+  names for big operators in Iris.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -80,6 +82,7 @@ s/\bmap_Forall_insert_11\b/map_Forall_insert_1_1/g
 s/\bmap_Forall_insert_12\b/map_Forall_insert_1_2/g
 s/\bmap_Forall_union_11\b/map_Forall_union_1_1/g
 s/\bmap_Forall_union_12\b/map_Forall_union_1_2/g
+s/\bForall_Forall2\b/Forall_Forall2_diag/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/list.v b/theories/list.v
index 4222076bb30ad9b23f707e4f4cb813242d8bc10b..d859626e4abd5f9b15854dae35d8c01b2197de37 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2735,7 +2735,7 @@ Proof.
 Qed.
 
 (** ** Properties of the [Forall2] predicate *)
-Lemma Forall_Forall2 {A} (Q : A → A → Prop) l :
+Lemma Forall_Forall2_diag {A} (Q : A → A → Prop) l :
   Forall (λ x, Q x x) l → Forall2 Q l l.
 Proof. induction 1; constructor; auto. Qed.
 
@@ -4645,7 +4645,7 @@ Ltac decompose_Forall := repeat
   | |- Forall _ (_ ++ _) => apply Forall_app_2
   | |- Forall _ (_ <$> _) => apply Forall_fmap
   | |- Forall _ (_ ≫= _) => apply Forall_bind
-  | |- Forall2 _ _ _ => apply Forall_Forall2
+  | |- Forall2 _ _ _ => apply Forall_Forall2_diag
   | |- Forall2 _ [] [] => constructor
   | |- Forall2 _ (_ :: _) (_ :: _) => constructor
   | |- Forall2 _ (_ ++ _) (_ ++ _) => first