From 878aa716ca33224ddc23826baee60000a269af03 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 2 Sep 2017 21:50:18 +0200
Subject: [PATCH] Also add a type class version of Forall.

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

diff --git a/theories/base.v b/theories/base.v
index dabf8bdb..9721f053 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.
-- 
GitLab