diff --git a/theories/list.v b/theories/list.v
index 50dcc652b12992cd9fb68e1481db1989ce369579..943ef18229dbbf7bcb5e84b520ad9f1e02fd6dc2 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.