From 2d27f42b9c4d9e5c0810122779a93873050fb756 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 2 Sep 2017 22:17:14 +0200
Subject: [PATCH] More TCForall lemmas.

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

diff --git a/theories/list.v b/theories/list.v
index 50dcc652..943ef182 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3489,6 +3489,13 @@ Proof.
   inversion_clear 1. rewrite reverse_cons, <-(assoc_L (++)). by apply IH.
 Qed.
 
+Lemma TCForall_Forall {A} (P : A → Prop) xs : TCForall P xs ↔ Forall P xs.
+Proof. split; induction 1; constructor; auto. Qed.
+
+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.
+
 (** * Relection over lists *)
 (** We define a simple data structure [rlist] to capture a syntactic
 representation of lists consisting of constants, applications and the nil list.
-- 
GitLab