From 7df279970018544311942d901eaaa78c8ebe6cb5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 6 Sep 2014 14:06:53 +0200
Subject: [PATCH] Add map_Forall3.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 9fcfe103..e0966cc0 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -84,6 +84,13 @@ Definition map_Forall2 `{∀ A, Lookup K A (M A)} {A B}
   | None, Some y => Q y
   | None, None => True
   end.
+Definition map_Forall3 `{∀ A, Lookup K A (M A)} {A B C}
+    (R : A → B → C → Prop) (m1 : M A) (m2 : M B) (m3 : M C): Prop := ∀ i,
+  match m1 !! i, m2 !! i, m3 !! i with
+  | Some x, Some y, Some z => R x y z
+  | None, None, None => True
+  | _, _, _ => False
+  end.
 
 Instance map_disjoint `{∀ A, Lookup K A (M A)} {A} : Disjoint (M A) :=
   map_Forall2 (λ _ _, False) (λ _, True) (λ _, True).
-- 
GitLab