From 1ed14abe59d584d8e12cbd9ec9509cd9b2498942 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Jan 2018 23:47:29 +0100
Subject: [PATCH] Lemmas for constructing a `Forall2` from a `Forall`.

---
 theories/list.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index 5b028f24..c0506bba 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.
-- 
GitLab