From 22e0ade784a83219f13b3545eff42ff0e0f9d86c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 6 Mar 2019 13:22:12 +0100
Subject: [PATCH] Removed unused argument for `map_seq` lemmas.
---
theories/fin_maps.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index bfdb78d5..6925e167 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1975,14 +1975,14 @@ Section map_seq.
- by rewrite IH, Nat.add_succ_r, !insert_union_singleton_l, (assoc_L _).
Qed.
- Lemma map_seq_cons_disjoint start xs x :
+ Lemma map_seq_cons_disjoint start xs :
map_seq (M:=M A) (S start) xs !! start = None.
Proof. rewrite lookup_map_seq_None. lia. Qed.
Lemma map_seq_cons start xs x :
map_seq start (x :: xs) =@{M A} <[start:=x]> (map_seq (S start) xs).
Proof. done. Qed.
- Lemma map_seq_snoc_disjoint start xs x :
+ Lemma map_seq_snoc_disjoint start xs :
map_seq (M:=M A) start xs !! (start+length xs) = None.
Proof. rewrite lookup_map_seq_None. lia. Qed.
Lemma map_seq_snoc start xs x :
--
GitLab