diff --git a/theories/list.v b/theories/list.v
index 8f05884b8d34c5de5a725966c918a2e3ce08b091..35967c3d8e8db8860d4050c4949c9aa304282a36 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.