From 0ac2b4db07bdc471421c5a4c47789087b3df074c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 17 Mar 2017 14:53:05 +0100
Subject: [PATCH] relate Forall2 and Forall

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

diff --git a/theories/list.v b/theories/list.v
index e1fe731f..e141ca94 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -2301,6 +2301,7 @@ Qed.
 Lemma Forall_Forall2 {A} (Q : A → A → Prop) l :
   Forall (λ x, Q x x) l → Forall2 Q l l.
 Proof. induction 1; constructor; auto. Qed.
+
 Lemma Forall2_forall `{Inhabited A} B C (Q : A → B → C → Prop) l k :
   Forall2 (λ x y, ∀ z, Q z x y) l k ↔ ∀ z, Forall2 (Q z) l k.
 Proof.
@@ -2310,6 +2311,10 @@ Proof.
   - apply IH. intros z. by feed inversion (Hlk z).
 Qed.
 
+Lemma Forall2_Forall {A} P (l1 l2 : list A) :
+  Forall2 P l1 l2 → Forall (curry P) (zip l1 l2).
+Proof. induction 1; constructor; auto. Qed.
+
 Section Forall2.
   Context {A B} (P : A → B → Prop).
   Implicit Types x : A.
-- 
GitLab