From 77cb2b8ac583aac43fab3c381f3e71acdf946343 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 15 Apr 2021 12:18:46 +0200
Subject: [PATCH] Add `map_seq_proper`.

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

diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 05eb4b04..7397ef32 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2417,6 +2417,15 @@ Section map_seq.
   Implicit Types x : A.
   Implicit Types xs : list A.
 
+  Global Instance map_seq_proper `{Equiv A} start :
+    Proper ((≡) ==> (≡)) (map_seq (M:=M A) start).
+  Proof.
+    intros l1 l2 Hl. revert start.
+    induction Hl as [|x1 x2 l1 l2 ?? IH]; intros start; simpl.
+    - intros ?. rewrite lookup_empty; constructor.
+    - repeat (done || f_equiv).
+  Qed.
+
   Lemma lookup_map_seq start xs i :
     map_seq (M:=M A) start xs !! i = guard (start ≤ i); xs !! (i - start).
   Proof.
-- 
GitLab