diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9b87bae3ebb6ab058ef8118abdd0215732452927..d859ddc67b05759f20fa3fd7816c077a4bf3368c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -158,6 +158,9 @@ API-breaking change is listed.
   application term.
 - Add map lookup lemmas: `lookup_union_is_Some`, `lookup_difference_is_Some`,
   `lookup_union_Some_l_inv`, `lookup_union_Some_r_inv`.
+- Make `Forall2_nil`, `Forall2_cons` bidirectional lemmas with `Forall2_nil_2`,
+  `Forall2_cons_2` being the original one-directional versions (matching
+  `Forall_nil` and `Forall_cons`). Rename `Forall2_cons_inv` to `Forall2_cons_1`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -210,6 +213,8 @@ s/\bgmultiset_elements_empty'\b/gmultiset_elements_empty_iff/g
 # map_filter_insert
 s/\bmap_filter_insert\b/map_filter_insert_True/g
 s/\bmap_filter_insert_not_delete\b/map_filter_insert_False/g
+# Forall2
+s/\bForall2_cons_inv\b/Forall2_cons_1/g
 EOF
 ```
 
diff --git a/theories/list.v b/theories/list.v
index 19068bc93225a35a8c920c78d5b12c99a01c4bcf..c6e0aeb46f6a221536ac07d3a6ea4ad44218c551 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2712,7 +2712,8 @@ Proof.
   end); clear go; intuition.
 Defined.
 
-(** Export the Coq stdlib constructors under different names. *)
+(** Export the Coq stdlib constructors under different names,
+because we use Forall_nil and Forall_cons for a version with a biimplication. *)
 Definition Forall_nil_2 := @Forall_nil A.
 Definition Forall_cons_2 := @Forall_cons A.
 Global Instance Forall_proper:
@@ -2984,7 +2985,8 @@ Lemma Forall2_Forall {A} P (l1 l2 : list A) :
   Forall2 P l1 l2 → Forall (uncurry P) (zip l1 l2).
 Proof. induction 1; constructor; auto. Qed.
 
-(** Export the Coq stdlib constructors under a different name *)
+(** Export the Coq stdlib constructors under a different name,
+because we use Forall_nil and Forall_cons for a version with a biimplication. *)
 Definition Forall2_nil_2 := @Forall2_nil.
 Definition Forall2_cons_2 := @Forall2_cons.
 Section Forall2.