1 files changed, 4 insertions, 10 deletions
diff --git a/FinMap.agda b/FinMap.agda
index 2a17519..8322b79 100644
--- a/FinMap.agda
+++ b/FinMap.agda
@@ -7,7 +7,7 @@ open import Data.Fin using (Fin ; zero ; suc)
 open import Data.Fin.Properties using (_≟_)
 open import Data.Vec using (Vec ; [] ; _∷_ ; _[_]≔_ ; replicate ; tabulate ; foldr ; zip ; toList) renaming (lookup to lookupVec ; map to mapV)
 open import Data.Vec.Equality using ()
-open import Data.Vec.Properties using (lookup∘update)
+open import Data.Vec.Properties using (lookup∘update ; lookup∘update′)
 open import Data.Product using (_×_ ; _,_)
 open import Data.List.All as All using (All)
 import Data.List.All.Properties as AllP
@@ -84,12 +84,6 @@ lemma-lookupM-empty : {A : Set} {n : ℕ} → (i : Fin n) → lookupM {A} i empt
 lemma-lookupM-empty zero    = refl
 lemma-lookupM-empty (suc i) = lemma-lookupM-empty i
 
-lemma-lookupM-insert-other : {A : Set} {n : ℕ} → (i j : Fin n) → (a : A) → (m : FinMapMaybe n A) → i ≢ j → lookupM i (insert j a m) ≡ lookupM i m
-lemma-lookupM-insert-other zero    zero    a m        p = contradiction refl p
-lemma-lookupM-insert-other zero    (suc j) a (x ∷ xs) p = refl
-lemma-lookupM-insert-other (suc i) zero    a (x ∷ xs) p = refl
-lemma-lookupM-insert-other (suc i) (suc j) a (x ∷ xs) p = lemma-lookupM-insert-other i j a xs (p ∘ cong suc)
-
 lemma-lookupM-restrict : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (is : Vec (Fin n) m) → {a : A} → lookupM i (restrict f is) ≡ just a → f i ≡ a
 lemma-lookupM-restrict i f []            p = contradiction (trans (sym p) (lemma-lookupM-empty i)) (λ ())
 lemma-lookupM-restrict i f (i' ∷ is)     p with i ≟ i'
@@ -101,7 +95,7 @@ lemma-lookupM-restrict i f (.i ∷ is) {a} p | yes refl = just-injective (begin
    just a ∎)
 lemma-lookupM-restrict i f (i' ∷ is) {a} p | no i≢i' = lemma-lookupM-restrict i f is (begin
   lookupM i (restrict f is)
-    ≡⟨ sym (lemma-lookupM-insert-other i i' (f i') (restrict f is) i≢i') ⟩
+    ≡⟨ sym (lookup∘update′ i≢i' (restrict f is) (just (f i'))) ⟩
   lookupM i (insert i' (f i') (restrict f is))
     ≡⟨ p ⟩
   just a ∎)
@@ -111,13 +105,13 @@ lemma-lookupM-restrict-∈ i f (j ∷ js)  p             with i ≟ j
 lemma-lookupM-restrict-∈ i f (.i ∷ js) p             | yes refl = lookup∘update i (restrict f js) (just (f i))
 lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.here i≡j) | no i≢j = contradiction i≡j i≢j
 lemma-lookupM-restrict-∈ i f (j ∷ js) (Any.there p)  | no i≢j =
-  trans (lemma-lookupM-insert-other i j (f j) (restrict f js) i≢j)
+  trans (lookup∘update′ i≢j (restrict f js) (just (f j)))
         (lemma-lookupM-restrict-∈ i f js p)
 
 lemma-lookupM-restrict-∉ : {A : Set} {n m : ℕ} → (i : Fin n) → (f : Fin n → A) → (js : Vec (Fin n) m) → i ∉ js → lookupM i (restrict f js) ≡ nothing
 lemma-lookupM-restrict-∉ i f []       i∉[]  = lemma-lookupM-empty i
 lemma-lookupM-restrict-∉ i f (j ∷ js) i∉jjs =
-  trans (lemma-lookupM-insert-other i j (f j) (restrict f js) (All.head i∉jjs))
+  trans (lookup∘update′ (All.head i∉jjs) (restrict f js) (just (f j)))
         (lemma-lookupM-restrict-∉ i f js (All.tail i∉jjs))
 
 lemma-tabulate-∘ : {n : ℕ} {A : Set} → {f g : Fin n → A} → f ≗ g → tabulate f ≡ tabulate g