From ea60af21ae805f2b0921fe591210679935ce6556 Mon Sep 17 00:00:00 2001
From: Helmut Grohne <grohne@cs.uni-bonn.de>
Date: Thu, 2 Jul 2015 11:51:37 +0200
Subject: split lemma-union-not-used into lemma-exchange-maps
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

New type suggested by Janis Voigtländer.
---
 FinMap.agda | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'FinMap.agda')

diff --git a/FinMap.agda b/FinMap.agda
index cbe24c5..ca7e73b 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -157,3 +157,7 @@ lemma-disjoint-union {n} f t = lemma-tabulate-∘ inner
           maybe′ just (lookupM x (fromFunc f)) nothing
             ≡⟨ lemma-lookupM-fromFunc f x ⟩
           just (f x) ∎
+
+lemma-exchange-maps : {n m : ℕ} → {A : Set} → {h h′ : FinMapMaybe n A} → {P : Fin n → Set} → (∀ j → P j → lookupM j h ≡ lookupM j h′) → {is : Vec (Fin n) m} → All P (toList is) → mapV (flip lookupM h) is ≡ mapV (flip lookupM h′) is
+lemma-exchange-maps h≈h′ {[]}     All.[]         = refl
+lemma-exchange-maps h≈h′ {i ∷ is} (pi All.∷ pis) = cong₂ _∷_ (h≈h′ i pi) (lemma-exchange-maps h≈h′ pis)
-- 
cgit v1.2.3