diff --git a/theories/base.v b/theories/base.v
index dabf8bdb10b60c357bf596b4b7f4172025730626..9721f053de6cdeded610e5031982a22666cbed4f 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -43,6 +43,13 @@ Inductive TCTrue : Prop := TCTrue_intro : TCTrue.
 Existing Class TCTrue.
 Existing Instance TCTrue_intro.
 
+Inductive TCForall {A} (P : A → Prop) : list A → Prop :=
+  | TCForall_nil : TCForall P []
+  | TCForall_cons x xs : P x → TCForall P xs → TCForall P (x :: xs).
+Existing Class TCForall.
+Existing Instance TCForall_nil.
+Existing Instance TCForall_cons.
+
 (** Throughout this development we use [C_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
 Delimit Scope C_scope with C.