From 81f9b1939dfe012638e63ba1c9c97653071729cb Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 30 Jan 2020 11:02:59 +0100
Subject: [PATCH] added tcforall2_forall lemma

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

diff --git a/theories/list.v b/theories/list.v
index 8f05884b..35967c3d 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3963,6 +3963,9 @@ Instance TCForall_app {A} (P : A → Prop) xs ys :
   TCForall P xs → TCForall P ys → TCForall P (xs ++ ys).
 Proof. rewrite !TCForall_Forall. apply Forall_app_2. Qed.
 
+Lemma TCForall2_Forall2 {A B} (P : A → B → Prop) xs ys : TCForall2 P xs ys ↔ Forall2 P xs ys.
+Proof. split; induction 1; constructor; auto. Qed.
+
 Section positives_flatten_unflatten.
   Local Open Scope positive_scope.
 
-- 
GitLab