diff --git a/theories/list.v b/theories/list.v
index 5b028f2473149bfb648a1ffbf4df8928b18456d5..c0506bba6768dfe6e3bb1d2adacb97db5059d145 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2409,6 +2409,13 @@ Section Forall2.
     intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto.
   Qed.
 
+  Lemma Forall_Forall2_l l k :
+    length l = length k → Forall (λ x, ∀ y, P x y) l → Forall2 P l k.
+  Proof. rewrite <-Forall2_same_length. induction 1; inversion 1; auto. Qed.
+  Lemma Forall_Forall2_r l k :
+    length l = length k → Forall (λ y, ∀ x, P x y) k → Forall2 P l k.
+  Proof. rewrite <-Forall2_same_length. induction 1; inversion 1; auto. Qed.
+
   Lemma Forall2_Forall_l (Q : A → Prop) l k :
     Forall2 P l k → Forall (λ y, ∀ x, P x y → Q x) k → Forall Q l.
   Proof. induction 1; inversion_clear 1; eauto. Qed.