From 42da66bfd3578e97451b8c9ac30530c38ba90ec6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 8 Dec 2017 18:30:24 +0100
Subject: [PATCH] Add `TCForall2`.

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

diff --git a/theories/base.v b/theories/base.v
index c30bbe82..763e86c4 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -91,6 +91,14 @@ Existing Class TCForall.
 Existing Instance TCForall_nil.
 Existing Instance TCForall_cons.
 
+Inductive TCForall2 {A B} (P : A → B → Prop) : list A → list B → Prop :=
+  | TCForall2_nil : TCForall2 P [] []
+  | TCForall2_cons x y xs ys :
+     P x y → TCForall2 P xs ys → TCForall2 P (x :: xs) (y :: ys).
+Existing Class TCForall2.
+Existing Instance TCForall2_nil.
+Existing Instance TCForall2_cons.
+
 (** Throughout this development we use [stdpp_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
 Delimit Scope stdpp_scope with stdpp.
-- 
GitLab