Prove that foldr is monotonic when input lists are pairwise monotonic

This should help prove that "join" is monotonic

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Lattice.agda

@@ -85,6 +85,20 @@ record IsSemilattice {a} (A : Set a)
     ≼-refl : ∀ (a : A) → a ≼ a
     ≼-refl a = ⊔-idemp a
 
+    ≼-trans : ∀ {a₁ a₂ a₃ : A} → a₁ ≼ a₂ → a₂ ≼ a₃ → a₁ ≼ a₃
+    ≼-trans {a₁} {a₂} {a₃} a₁≼a₂ a₂≼a₃ =
+        begin
+            a₁ ⊔ a₃
+        ∼⟨ ≈-⊔-cong ≈-refl (≈-sym a₂≼a₃) ⟩
+            a₁ ⊔ (a₂ ⊔ a₃)
+        ∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
+            (a₁ ⊔ a₂) ⊔ a₃
+        ∼⟨ ≈-⊔-cong a₁≼a₂ ≈-refl ⟩
+            a₂ ⊔ a₃
+        ∼⟨ a₂≼a₃ ⟩
+            a₃
+        ∎
+
     ≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄
     ≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁⊔a₃≈a₃ =
         begin
@@ -118,11 +132,24 @@ module _ {a b} {A : Set a} {B : Set b}
          (lA : IsSemilattice A _≈₁_ _⊔₁_) (lB : IsSemilattice B _≈₂_ _⊔₂_) where
 
     open IsSemilattice lA using () renaming (_≼_ to _≼₁_)
-    open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp)
+    open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)
 
     const-Mono : ∀ (x : B) → Monotonic _≼₁_ _≼₂_ (λ _ → x)
     const-Mono x _ = ⊔₂-idemp x
 
+    open import Data.List as List using (List; foldr; _∷_)
+    open import Utils using (Pairwise; _∷_)
+
+    foldr-Mono : ∀ (l₁ l₂ : List A) (f : A → B → B) (b₁ b₂ : B) →
+                 Pairwise _≼₁_ l₁ l₂ → b₁ ≼₂ b₂ →
+                 (∀ b → Monotonic _≼₁_ _≼₂_ (λ a → f a b)) →
+                 (∀ a → Monotonic _≼₂_ _≼₂_ (f a)) →
+                 foldr f b₁ l₁ ≼₂ foldr f b₂ l₂
+    foldr-Mono List.[] List.[] f b₁ b₂ _ b₁≼b₂ _ _ = b₁≼b₂
+    foldr-Mono (x ∷ xs) (y ∷ ys) f b₁ b₂ (x≼y ∷ xs≼ys) b₁≼b₂ f-Mono₁ f-Mono₂ =
+        ≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y)
+                 (f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂))
+
 record IsLattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A)
@@ -146,6 +173,7 @@ record IsLattice {a} (A : Set a)
         ; _≼_ to _≽_
         ; _≺_ to _≻_
         ; ≼-refl to ≽-refl
+        ; ≼-trans to ≽-trans
         )
 
     FixedHeight : ∀ (h : ℕ) → Set a

Lattice/FiniteValueMap.agda

@@ -36,6 +36,7 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
         ; _∈_
         ; Map-functional
         ; Expr-Provenance
+        ; Expr-Provenance-≡
         ; _∩_; _∪_; `_
         ; in₁; in₂; bothᵘ; single
         ; ⊔-combines
@@ -184,7 +185,7 @@ module IterProdIsomorphism where
                 narrow₂ {fm₁} {fm₂ = (_ ∷ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
                     with kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
                 ...   | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) =
-                        ⊥-elim (All¬-¬Any k≢ks (forget {m = proj₁ fm₁} k',v'∈fm'₁))
+                        ⊥-elim (All¬-¬Any k≢ks (forget k',v'∈fm'₁))
                 ...   | (v'' , (v'≈v'' , there k',v'∈fm'₂)) =
                         (v'' , (v'≈v'' , k',v'∈fm'₂))
 
@@ -195,7 +196,7 @@ module IterProdIsomorphism where
         k,v∈pop⇒k,v∈ : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) →
                        (k' , v) ∈ᵐ pop fm → (¬ k ≡ k' × ((k' , v) ∈ᵐ fm))
         k,v∈pop⇒k,v∈ {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k',v∈fm =
-            ( (λ { refl → All¬-¬Any k≢ks (forget {m = (fm' , uks')} k',v∈fm) })
+            ( (λ { refl → All¬-¬Any k≢ks (forget k',v∈fm) })
             , there k',v∈fm
             )
 
@@ -212,17 +213,16 @@ module IterProdIsomorphism where
         Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} →
                            (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → FromBothMaps k v fm₁ fm₂
         Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
-            with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂)
+            with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂
-        ...   | (_ , (in₁ (single k,v∈m₁) k∉km₂ , _))
+        ...   | in₁ (single k,v∈m₁) k∉km₂
-                with k∈km₁ ← (forget {m = m₁} k,v∈m₁)
+                with k∈km₁ ← (forget k,v∈m₁)
                 rewrite trans ks₁≡ks (sym ks₂≡ks) =
                 ⊥-elim (k∉km₂ k∈km₁)
-        ...   | (_ , (in₂ k∉km₁ (single k,v∈m₂) , _))
+        ...   | in₂ k∉km₁ (single k,v∈m₂)
-                with k∈km₂ ← (forget {m = m₂} k,v∈m₂)
+                with k∈km₂ ← (forget k,v∈m₂)
                 rewrite trans ks₁≡ks (sym ks₂≡ks) =
                 ⊥-elim (k∉km₁ k∈km₂)
-        ...   | (v₁⊔v₂ , (bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) , k,v₁⊔v₂∈m₁m₂))
+        ...   | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
-                rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂ =
                 ((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
 
         pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) →
@@ -324,11 +324,9 @@ module IterProdIsomorphism where
           | from-first-value (fm₁ ⊔ᵐ fm₂)
           | from-first-value fm₁ | from-first-value fm₂
     ...   | (v , k,v∈fm₁fm₂) | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl | refl
-            with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂)
+            with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget k,v∈fm₁fm₂)
-    ...       | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget {m = m₂}
+    ...       | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget k,v₂∈fm₂))
-                                                                k,v₂∈fm₂))
+    ...       | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget k,v₁∈fm₁))
-    ...       | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget {m = m₁}
-                                                                k,v₁∈fm₁))
     ...       | (v₁⊔v₂ , (bothᵘ {v₁'} {v₂'} (single k,v₁'∈m₁) (single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂))
                 rewrite Map-functional {m = m₁} k,v₁∈fm₁ k,v₁'∈m₁
                 rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₂'∈m₂
@@ -387,10 +385,10 @@ module IterProdIsomorphism where
                     (v , (IsLattice.≈-refl lB , here refl))
             ...   | here refl | there k',v₂∈fm₂' =
                     ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₂')
-                                                   (forget {m = proj₁ fm₂'} k',v₂∈fm₂')))
+                                                   (forget k',v₂∈fm₂')))
             ...   | there k',v₁∈fm₁' | here refl =
                     ⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁')
-                                                   (forget {m = proj₁ fm₁'} k',v₁∈fm₁')))
+                                                   (forget k',v₁∈fm₁')))
             ...   | there k',v₁∈fm₁' | there k',v₂∈fm₂' =
                         let
                             k',v₁v₂∈fm₁'fm₂' =

Lattice/Map.agda

@@ -488,7 +488,9 @@ _∈k_ k m = MemProp._∈_ k (keys m)
 locate : ∀ {k : A} {m : Map} → k ∈k m → Σ B (λ v → (k , v) ∈ m)
 locate k∈km = locate-impl k∈km
 
-forget : ∀ {k : A} {v : B} {m : Map} → (k , v) ∈ m → k ∈k m
+-- defined this way because ∈ for maps uses projection, so the full map can't be guessed.
+-- On the other hand, list can be guessed.
+forget : ∀ {k : A} {v : B} {l : List (A × B)} → (k , v) ∈ˡ l → k ∈ˡ (ImplKeys.keys l)
 forget = ∈-cong proj₁
 
 Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v'
@@ -592,9 +594,9 @@ Expr-Provenance k (e₁ ∩ e₂) k∈ke₁e₂
 ...   | no k∉ke₁ | yes k∈ke₂ = ⊥-elim (intersect-preserves-∉₁ {l₂ = proj₁ ⟦ e₂ ⟧} k∉ke₁ k∈ke₁e₂)
 ...   | no k∉ke₁ | no k∉ke₂ = ⊥-elim (intersect-preserves-∉₂ {l₁ = proj₁ ⟦ e₁ ⟧} k∉ke₂ k∈ke₁e₂)
 
-Expr-Provenance-≡ : ∀ (k : A) (v : B) (e : Expr) → (k , v) ∈ ⟦ e ⟧ → Provenance k v e
+Expr-Provenance-≡ : ∀ {k : A} {v : B} (e : Expr) → (k , v) ∈ ⟦ e ⟧ → Provenance k v e
-Expr-Provenance-≡ k v e k,v∈e
+Expr-Provenance-≡ {k} {v} e k,v∈e
-    with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget {m = ⟦ e ⟧} k,v∈e)
+    with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget k,v∈e)
     rewrite Map-functional {m = ⟦ e ⟧} k,v∈e k,v'∈e = p
 
 module _ (≈₂-dec : IsDecidable _≈₂_) where
@@ -609,7 +611,7 @@ module _ (≈₂-dec : IsDecidable _≈₂_) where
             let (v , k,v∈m₁) = locate-impl k∈km₁
             in no (λ m₁⊆m₂ →
                    let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
-                   in k∉km₂ (∈-cong proj₁ k,v'∈m₂))
+                   in k∉km₂ (forget k,v'∈m₂))
         SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) =
             no (λ m₁⊆m₂ →
                 let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁
@@ -665,19 +667,16 @@ private module I⊓ = ImplInsert _⊓₂_
 
         ⊔-⊆ : ∀ (m₁ m₂ m₃ m₄ : Map) → m₁ ≈ m₂ → m₃ ≈ m₄ → (m₁ ⊔ m₃) ⊆ (m₂ ⊔ m₄)
         ⊔-⊆ m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
-            with Expr-Provenance k ((` m₁) ∪ (` m₃)) (∈-cong proj₁ k,v∈m₁m₃)
+            with Expr-Provenance-≡ ((` m₁) ∪ (` m₃)) k,v∈m₁m₃
-        ...   | (_ , (bothᵘ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) , v₁v₃∈m₁m₃))
+        ...   | bothᵘ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) =
-                rewrite Map-functional {m = m₁ ⊔ m₃} k,v∈m₁m₃ v₁v₃∈m₁m₃ =
                 let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
                     (v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
                 in (v₂ ⊔₂ v₄ , (≈₂-⊔₂-cong v₁≈v₂ v₃≈v₄ , I⊔.union-combines (proj₂ m₂) (proj₂ m₄) k,v₂∈m₂ k,v₄∈m₄))
-        ...   | (_ , (in₁ (single {v₁} v₁∈m₁) k∉km₃ , v₁∈m₁m₃))
+        ...   | in₁ (single {v₁} v₁∈m₁) k∉km₃ =
-                rewrite Map-functional {m = m₁ ⊔ m₃} k,v∈m₁m₃ v₁∈m₁m₃ =
                 let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
                     k∉km₄ = ≈-∉-cong {m₃} {m₄} m₃≈m₄ k∉km₃
                 in (v₂ , (v₁≈v₂ , I⊔.union-preserves-∈₁ (proj₂ m₂) k,v₂∈m₂ k∉km₄))
-        ...   | (_ , (in₂ k∉km₁ (single {v₃} v₃∈m₃) , v₃∈m₁m₃))
+        ...   | in₂ k∉km₁ (single {v₃} v₃∈m₃) =
-                rewrite Map-functional {m = m₁ ⊔ m₃} k,v∈m₁m₃ v₃∈m₁m₃ =
                 let (v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
                     k∉km₂ = ≈-∉-cong {m₁} {m₂} m₁≈m₂ k∉km₁
                 in (v₄ , (v₃≈v₄ , I⊔.union-preserves-∈₂ k∉km₂ k,v₄∈m₄))
@@ -690,9 +689,8 @@ private module I⊓ = ImplInsert _⊓₂_
     where
         ⊓-⊆ : ∀ (m₁ m₂ m₃ m₄ : Map) → m₁ ≈ m₂ → m₃ ≈ m₄ → (m₁ ⊓ m₃) ⊆ (m₂ ⊓ m₄)
         ⊓-⊆ m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
-            with Expr-Provenance k ((` m₁) ∩ (` m₃)) (∈-cong proj₁ k,v∈m₁m₃)
+            with Expr-Provenance-≡ ((` m₁) ∩ (` m₃)) k,v∈m₁m₃
-        ...   | (_ , (bothⁱ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) , v₁v₃∈m₁m₃))
+        ...   | bothⁱ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) =
-                rewrite Map-functional {m = m₁ ⊓ m₃} k,v∈m₁m₃ v₁v₃∈m₁m₃ =
                 let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
                     (v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
                 in (v₂ ⊓₂ v₄ , (≈₂-⊓₂-cong v₁≈v₂ v₃≈v₄ , I⊓.intersect-combines (proj₂ m₂) (proj₂ m₄) k,v₂∈m₂ k,v₄∈m₄))
@@ -702,13 +700,12 @@ private module I⊓ = ImplInsert _⊓₂_
     where
         mm-m-⊆ : (m ⊔ m) ⊆ m
         mm-m-⊆ k v k,v∈mm
-            with Expr-Provenance k ((` m) ∪ (` m)) (∈-cong proj₁ k,v∈mm)
+            with Expr-Provenance-≡ ((` m) ∪ (` m)) k,v∈mm
-        ...   | (_ , (bothᵘ (single {v'} v'∈m) (single {v''} v''∈m) , v'v''∈mm))
+        ...   | bothᵘ (single {v'} v'∈m) (single {v''} v''∈m)
-                rewrite Map-functional {m = m} v'∈m v''∈m
+                rewrite Map-functional {m = m} v'∈m v''∈m =
-                rewrite Map-functional {m = m ⊔ m} k,v∈mm v'v''∈mm =
                 (v'' , (⊔₂-idemp v'' , v''∈m))
-        ...   | (_ , (in₁ (single {v'} v'∈m) k∉km , _)) = ⊥-elim (k∉km (∈-cong proj₁ v'∈m))
+        ...   | in₁ (single {v'} v'∈m) k∉km = ⊥-elim (k∉km (∈-cong proj₁ v'∈m))
-        ...   | (_ , (in₂ k∉km (single {v''} v''∈m) , _)) = ⊥-elim (k∉km (∈-cong proj₁ v''∈m))
+        ...   | in₂ k∉km (single {v''} v''∈m) = ⊥-elim (k∉km (∈-cong proj₁ v''∈m))
 
         m-mm-⊆ : m ⊆ (m ⊔ m)
         m-mm-⊆ k v k,v∈m = (v ⊔₂ v , (≈₂-sym (⊔₂-idemp v) , I⊔.union-combines u u k,v∈m k,v∈m))
@@ -718,15 +715,12 @@ private module I⊓ = ImplInsert _⊓₂_
     where
         ⊔-comm-⊆ : ∀ (m₁ m₂ : Map) → (m₁ ⊔ m₂) ⊆ (m₂ ⊔ m₁)
         ⊔-comm-⊆ m₁@(l₁ , u₁) m₂@(l₂ , u₂) k v k,v∈m₁m₂
-            with Expr-Provenance k ((` m₁) ∪ (` m₂)) (∈-cong proj₁ k,v∈m₁m₂)
+            with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈m₁m₂
-        ...   | (_ , (bothᵘ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) , v₁v₂∈m₁m₂))
+        ...   | bothᵘ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) =
-                rewrite Map-functional {m = m₁ ⊔ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂ =
                 (v₂ ⊔₂ v₁ , (⊔₂-comm v₁ v₂ , I⊔.union-combines u₂ u₁ v₂∈m₂ v₁∈m₁))
-        ...   | (_ , (in₁ {v₁} (single v₁∈m₁) k∉km₂ , v₁∈m₁m₂))
+        ...   | in₁ {v₁} (single v₁∈m₁) k∉km₂ =
-                rewrite Map-functional {m = m₁ ⊔ m₂} k,v∈m₁m₂ v₁∈m₁m₂ =
                 (v₁ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉km₂ v₁∈m₁))
-        ...   | (_ , (in₂ {v₂} k∉km₁ (single v₂∈m₂) , v₂∈m₁m₂))
+        ...   | in₂ {v₂} k∉km₁ (single v₂∈m₂) =
-                rewrite Map-functional {m = m₁ ⊔ m₂} k,v∈m₁m₂ v₂∈m₁m₂ =
                 (v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ u₂ v₂∈m₂ k∉km₁))
 
 ⊔-assoc : ∀ (m₁ m₂ m₃ : Map) → ((m₁ ⊔ m₂) ⊔ m₃) ≈ (m₁ ⊔ (m₂ ⊔ m₃))
@@ -734,54 +728,40 @@ private module I⊓ = ImplInsert _⊓₂_
     where
         ⊔-assoc₁ : ((m₁ ⊔ m₂) ⊔ m₃) ⊆ (m₁ ⊔ (m₂ ⊔ m₃))
         ⊔-assoc₁ k v k,v∈m₁₂m₃
-            with Expr-Provenance k (((` m₁) ∪ (` m₂)) ∪ (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
+            with Expr-Provenance-≡ (((` m₁) ∪ (` m₂)) ∪ (` m₃)) k,v∈m₁₂m₃
-        ...   | (_ , (in₂ k∉ke₁₂ (single {v₃} v₃∈e₃) , v₃∈m₁₂m₃))
+        ...   | in₂ k∉ke₁₂ (single {v₃} v₃∈e₃) =
-                rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₃∈m₁₂m₃ =
                 let (k∉ke₁ , k∉ke₂) = I⊔.∉-union-∉-either {l₁ = l₁} {l₂ = l₂} k∉ke₁₂
                 in (v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-preserves-∈₂ k∉ke₂ v₃∈e₃)))
-        ...   | (_ , (in₁ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke₃ , v₂∈m₁₂m₃))
+        ...   | in₁ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke₃ =
-                rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₂∈m₁₂m₃ =
                 (v₂ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-preserves-∈₁ u₂ v₂∈e₂ k∉ke₃)))
-        ...   | (_ , (bothᵘ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₂v₃∈m₁₂m₃))
+        ...   | bothᵘ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
-                rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₂v₃∈m₁₂m₃ =
                 (v₂ ⊔₂ v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁  (I⊔.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
-        ...   | (_ , (in₁ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ , v₁∈m₁₂m₃))
+        ...   | in₁ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ =
-                rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁∈m₁₂m₃ =
                 (v₁ , (≈₂-refl , I⊔.union-preserves-∈₁ u₁ v₁∈e₁ (I⊔.union-preserves-∉ k∉ke₂ k∉ke₃)))
-        ...   | (_ , (bothᵘ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) , v₁v₃∈m₁₂m₃))
+        ...   | bothᵘ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) =
-                rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁v₃∈m₁₂m₃ =
                 (v₁ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-preserves-∈₂ k∉ke₂ v₃∈e₃)))
-        ...   | (_ , (in₁ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃), v₁v₂∈m₁₂m₃)
+        ...   | in₁ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃ =
-                rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁v₂∈m₁₂m₃ =
                 (v₁ ⊔₂ v₂ , (≈₂-refl , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-preserves-∈₁ u₂ v₂∈e₂ k∉ke₃)))
-        ...   | (_ , (bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
+        ...   | bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
-                rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
                 (v₁ ⊔₂ (v₂ ⊔₂ v₃) , (⊔₂-assoc v₁ v₂ v₃ , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
 
         ⊔-assoc₂ : (m₁ ⊔ (m₂ ⊔ m₃)) ⊆ ((m₁ ⊔ m₂) ⊔ m₃)
         ⊔-assoc₂ k v k,v∈m₁m₂₃
-            with Expr-Provenance k ((` m₁) ∪ ((` m₂) ∪ (` m₃))) (∈-cong proj₁ k,v∈m₁m₂₃)
+            with Expr-Provenance-≡ ((` m₁) ∪ ((` m₂) ∪ (` m₃))) k,v∈m₁m₂₃
-        ...   | (_ , (in₂ k∉ke₁ (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) , v₃∈m₁m₂₃))
+        ...   | in₂ k∉ke₁ (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) =
-                rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₃∈m₁m₂₃ =
                 (v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ (I⊔.union-preserves-∉ k∉ke₁ k∉ke₂) v₃∈e₃))
-        ...   | (_ , (in₂ k∉ke₁ (in₁ (single {v₂} v₂∈e₂) k∉ke₃) , v₂∈m₁m₂₃))
+        ...   | in₂ k∉ke₁ (in₁ (single {v₂} v₂∈e₂) k∉ke₃) =
-                rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₂∈m₁m₂₃ =
                 (v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) (I⊔.union-preserves-∈₂ k∉ke₁ v₂∈e₂) k∉ke₃))
-        ...   | (_ , (in₂ k∉ke₁ (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₂v₃∈m₁m₂₃))
+        ...   | in₂ k∉ke₁ (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
-                rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₂v₃∈m₁m₂₃ =
                 (v₂ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines (I⊔.union-preserves-Unique l₁ l₂ u₂) u₃ (I⊔.union-preserves-∈₂ k∉ke₁ v₂∈e₂) v₃∈e₃))
-        ...   | (_ , (in₁ (single {v₁} v₁∈e₁) k∉ke₂₃ , v₁∈m₁m₂₃))
+        ...   | in₁ (single {v₁} v₁∈e₁) k∉ke₂₃ =
-                rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁∈m₁m₂₃ =
                 let (k∉ke₂ , k∉ke₃) = I⊔.∉-union-∉-either {l₁ = l₂} {l₂ = l₃} k∉ke₂₃
                 in (v₁ , (≈₂-refl , I⊔.union-preserves-∈₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) (I⊔.union-preserves-∈₁ u₁ v₁∈e₁ k∉ke₂) k∉ke₃))
-        ...   | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) , v₁v₃∈m₁m₂₃))
+        ...   | bothᵘ (single {v₁} v₁∈e₁) (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) =
-                rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁v₃∈m₁m₂₃ =
                 (v₁ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines (I⊔.union-preserves-Unique l₁ l₂ u₂) u₃ (I⊔.union-preserves-∈₁ u₁ v₁∈e₁ k∉ke₂) v₃∈e₃))
-        ...   | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in₁ (single {v₂} v₂∈e₂) k∉ke₃) , v₁v₂∈m₁m₂₃))
+        ...   | bothᵘ (single {v₁} v₁∈e₁) (in₁ (single {v₂} v₂∈e₂) k∉ke₃) =
-                rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁v₂∈m₁m₂₃ =
                 (v₁ ⊔₂ v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) (I⊔.union-combines u₁ u₂ v₁∈e₁ v₂∈e₂) k∉ke₃))
-        ...   | (_ , (bothᵘ (single {v₁} v₁∈e₁) (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₁v₂v₃∈m₁m₂₃))
+        ...   | bothᵘ (single {v₁} v₁∈e₁) (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
-                rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁v₂v₃∈m₁m₂₃ =
                 ((v₁ ⊔₂ v₂) ⊔₂ v₃ , (≈₂-sym (⊔₂-assoc v₁ v₂ v₃) , I⊔.union-combines (I⊔.union-preserves-Unique l₁ l₂ u₂) u₃ (I⊔.union-combines u₁ u₂ v₁∈e₁ v₂∈e₂) v₃∈e₃))
 
 ⊓-idemp : ∀ (m : Map) → (m ⊓ m) ≈ m
@@ -789,10 +769,9 @@ private module I⊓ = ImplInsert _⊓₂_
     where
         mm-m-⊆ : (m ⊓ m) ⊆ m
         mm-m-⊆ k v k,v∈mm
-            with Expr-Provenance k ((` m) ∩ (` m)) (∈-cong proj₁ k,v∈mm)
+            with Expr-Provenance-≡ ((` m) ∩ (` m)) k,v∈mm
-        ...   | (_ , (bothⁱ (single {v'} v'∈m) (single {v''} v''∈m) , v'v''∈mm))
+        ...   | bothⁱ (single {v'} v'∈m) (single {v''} v''∈m)
-                rewrite Map-functional {m = m} v'∈m v''∈m
+                rewrite Map-functional {m = m} v'∈m v''∈m =
-                rewrite Map-functional {m = m ⊓ m} k,v∈mm v'v''∈mm =
                 (v'' , (⊓₂-idemp v'' , v''∈m))
 
         m-mm-⊆ : m ⊆ (m ⊓ m)
@@ -803,9 +782,8 @@ private module I⊓ = ImplInsert _⊓₂_
     where
         ⊓-comm-⊆ : ∀ (m₁ m₂ : Map) → (m₁ ⊓ m₂) ⊆ (m₂ ⊓ m₁)
         ⊓-comm-⊆ m₁@(l₁ , u₁) m₂@(l₂ , u₂) k v k,v∈m₁m₂
-            with Expr-Provenance k ((` m₁) ∩ (` m₂)) (∈-cong proj₁ k,v∈m₁m₂)
+            with Expr-Provenance-≡ ((` m₁) ∩ (` m₂)) k,v∈m₁m₂
-        ...   | (_ , (bothⁱ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) , v₁v₂∈m₁m₂))
+        ...   | bothⁱ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) =
-                rewrite Map-functional {m = m₁ ⊓ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂ =
                 (v₂ ⊓₂ v₁ , (⊓₂-comm v₁ v₂ , I⊓.intersect-combines u₂ u₁ v₂∈m₂ v₁∈m₁))
 
 ⊓-assoc : ∀ (m₁ m₂ m₃ : Map) → ((m₁ ⊓ m₂) ⊓ m₃) ≈ (m₁ ⊓ (m₂ ⊓ m₃))
@@ -813,16 +791,14 @@ private module I⊓ = ImplInsert _⊓₂_
     where
         ⊓-assoc₁ : ((m₁ ⊓ m₂) ⊓ m₃) ⊆ (m₁ ⊓ (m₂ ⊓ m₃))
         ⊓-assoc₁ k v k,v∈m₁₂m₃
-            with Expr-Provenance k (((` m₁) ∩ (` m₂)) ∩ (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
+            with Expr-Provenance-≡ (((` m₁) ∩ (` m₂)) ∩ (` m₃)) k,v∈m₁₂m₃
-        ...   | (_ , (bothⁱ (bothⁱ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
+        ...   | bothⁱ (bothⁱ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
-                rewrite Map-functional {m = (m₁ ⊓ m₂) ⊓ m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
                 (v₁ ⊓₂ (v₂ ⊓₂ v₃) , (⊓₂-assoc v₁ v₂ v₃ , I⊓.intersect-combines u₁ (I⊓.intersect-preserves-Unique {l₂} {l₃} u₃) v₁∈e₁ (I⊓.intersect-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
 
         ⊓-assoc₂ : (m₁ ⊓ (m₂ ⊓ m₃)) ⊆ ((m₁ ⊓ m₂) ⊓ m₃)
         ⊓-assoc₂ k v k,v∈m₁m₂₃
-            with Expr-Provenance k ((` m₁) ∩ ((` m₂) ∩ (` m₃))) (∈-cong proj₁ k,v∈m₁m₂₃)
+            with Expr-Provenance-≡ ((` m₁) ∩ ((` m₂) ∩ (` m₃))) k,v∈m₁m₂₃
-        ...   | (_ , (bothⁱ (single {v₁} v₁∈e₁) (bothⁱ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₁v₂v₃∈m₁m₂₃))
+        ...   | bothⁱ (single {v₁} v₁∈e₁) (bothⁱ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
-                rewrite Map-functional {m = m₁ ⊓ (m₂ ⊓ m₃)} k,v∈m₁m₂₃ v₁v₂v₃∈m₁m₂₃ =
                 ((v₁ ⊓₂ v₂) ⊓₂ v₃ , (≈₂-sym (⊓₂-assoc v₁ v₂ v₃) , I⊓.intersect-combines (I⊓.intersect-preserves-Unique {l₁} {l₂} u₂) u₃ (I⊓.intersect-combines u₁ u₂ v₁∈e₁ v₂∈e₂) v₃∈e₃))
 
 absorb-⊓-⊔ : ∀ (m₁ m₂ : Map) →  (m₁ ⊓ (m₁ ⊔ m₂)) ≈ m₁
@@ -830,20 +806,18 @@ absorb-⊓-⊔ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊓-⊔¹ , absor
     where
         absorb-⊓-⊔¹ : (m₁ ⊓ (m₁ ⊔ m₂)) ⊆ m₁
         absorb-⊓-⊔¹ k v k,v∈m₁m₁₂
-            with Expr-Provenance k ((` m₁) ∩ ((` m₁) ∪ (` m₂))) (∈-cong proj₁ k,v∈m₁m₁₂)
+            with Expr-Provenance-≡ ((` m₁) ∩ ((` m₁) ∪ (` m₂))) k,v∈m₁m₁₂
-        ...   | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
+        ...   | bothⁱ (single {v₁} k,v₁∈m₁)
                       (bothᵘ (single {v₁'} k,v₁'∈m₁)
-                                   (single {v₂} v₂∈m₂)) , v₁v₁'v₂∈m₁m₁₂))
+                             (single {v₂} v₂∈m₂))
-                rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
+                rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
-                rewrite Map-functional {m = m₁ ⊓ (m₁ ⊔ m₂)} k,v∈m₁m₁₂ v₁v₁'v₂∈m₁m₁₂ =
                 (v₁' , (absorb-⊓₂-⊔₂ v₁' v₂ , k,v₁'∈m₁))
-        ...   | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
+        ...   | bothⁱ (single {v₁} k,v₁∈m₁)
-                            (in₁ (single {v₁'} k,v₁'∈m₁) _) , v₁v₁'∈m₁m₁₂))
+                      (in₁ (single {v₁'} k,v₁'∈m₁) _)
-                rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
+                rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
-                rewrite Map-functional {m = m₁ ⊓ (m₁ ⊔ m₂)} k,v∈m₁m₁₂ v₁v₁'∈m₁m₁₂ =
                 (v₁' , (⊓₂-idemp v₁' , k,v₁'∈m₁))
-        ...   | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
+        ...   | bothⁱ (single {v₁} k,v₁∈m₁)
-                            (in₂ k∉m₁ _ ) , _)) = ⊥-elim (k∉m₁ (∈-cong proj₁ k,v₁∈m₁))
+                      (in₂ k∉m₁ _ ) = ⊥-elim (k∉m₁ (∈-cong proj₁ k,v₁∈m₁))
 
         absorb-⊓-⊔² : m₁ ⊆ (m₁ ⊓ (m₁ ⊔ m₂))
         absorb-⊓-⊔² k v k,v∈m₁
@@ -858,18 +832,16 @@ absorb-⊔-⊓ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊔-⊓¹ , absor
     where
         absorb-⊔-⊓¹ : (m₁ ⊔ (m₁ ⊓ m₂)) ⊆ m₁
         absorb-⊔-⊓¹ k v k,v∈m₁m₁₂
-            with Expr-Provenance k ((` m₁) ∪ ((` m₁) ∩ (` m₂))) (∈-cong proj₁ k,v∈m₁m₁₂)
+            with Expr-Provenance-≡ ((` m₁) ∪ ((` m₁) ∩ (` m₂))) k,v∈m₁m₁₂
-        ...   | (_ , (bothᵘ (single {v₁} k,v₁∈m₁)
+        ...   | bothᵘ (single {v₁} k,v₁∈m₁)
                       (bothⁱ (single {v₁'} k,v₁'∈m₁)
-                                   (single {v₂} k,v₂∈m₂)) , v₁v₁'v₂∈m₁m₁₂))
+                             (single {v₂} k,v₂∈m₂))
-                rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
+                rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
-                rewrite Map-functional {m = m₁ ⊔ (m₁ ⊓ m₂)} k,v∈m₁m₁₂ v₁v₁'v₂∈m₁m₁₂ =
                 (v₁' , (absorb-⊔₂-⊓₂ v₁' v₂ , k,v₁'∈m₁))
-        ...   | (_ , (in₁ (single {v₁} k,v₁∈m₁) k∉km₁₂ , k,v₁∈m₁m₁₂))
+        ...   | in₁ (single {v₁} k,v₁∈m₁) k∉km₁₂ =
-                rewrite Map-functional {m = m₁ ⊔ (m₁ ⊓ m₂)} k,v∈m₁m₁₂ k,v₁∈m₁m₁₂ =
                 (v₁ , (≈₂-refl , k,v₁∈m₁))
-        ...   | (_ , (in₂ k∉km₁ (bothⁱ (single {v₁'} k,v₁'∈m₁)
+        ...   | in₂ k∉km₁ (bothⁱ (single {v₁'} k,v₁'∈m₁)
-                                      (single {v₂} k,v₂∈m₂)) , _)) =
+                                (single {v₂} k,v₂∈m₂)) =
                 ⊥-elim (k∉km₁ (∈-cong proj₁ k,v₁'∈m₁))
 
         absorb-⊔-⊓² : m₁ ⊆ (m₁ ⊔ (m₁ ⊓ m₂))
@@ -1009,7 +981,7 @@ updating-via-k∈ks-forward m {ks} f k∈ks k∈km rewrite transform-keys-≡ (p
 updating-via-k∈ks-≡ : ∀ (m : Map) {ks : List A} (f : A → B) {k : A} {v : B} →
                     k ∈ˡ ks → (k , v) ∈ (m updating ks via f)→ v ≡ f k
 updating-via-k∈ks-≡ m {ks} f k∈ks k,v∈um
-    with updating-via-k∈ks m f k∈ks (forget {m = (m updating ks via f)} k,v∈um)
+    with updating-via-k∈ks m f k∈ks (forget k,v∈um)
 ...   | k,fk∈um = Map-functional {m = (m updating ks via f)} k,v∈um k,fk∈um
 
 updating-via-k∉ks-forward : ∀ (m : Map) {ks : List A} (f : A → B) {k : A} {v : B} →
@@ -1044,14 +1016,14 @@ module _ {l} {L : Set l}
 
                 f'l₁f'l₂⊆f'l₂ : ((f' l₁) ⊔ (f' l₂)) ⊆ f' l₂
                 f'l₁f'l₂⊆f'l₂ k v k,v∈f'l₁f'l₂
-                    with Expr-Provenance-≡ k v ((` (f' l₁)) ∪ (` (f' l₂))) k,v∈f'l₁f'l₂
+                    with Expr-Provenance-≡ ((` (f' l₁)) ∪ (` (f' l₂))) k,v∈f'l₁f'l₂
                 ...   | in₁ (single k,v∈f'l₁) k∉kf'l₂ =
                         let
-                            k∈kfl₁ = updating-via-∈k-backward (f l₁) ks (updater l₁) (forget {m = f' l₁} k,v∈f'l₁)
+                            k∈kfl₁ = updating-via-∈k-backward (f l₁) ks (updater l₁) (forget k,v∈f'l₁)
                             k∈kfl₁fl₂ = union-preserves-∈k₁ {l₁ = proj₁ (f l₁)} {l₂ = proj₁ (f l₂)} k∈kfl₁
                             (v' , k,v'∈fl₁l₂) = locate {m = (f l₁ ⊔ f l₂)} k∈kfl₁fl₂
                             (v'' , (v'≈v'' , k,v''∈fl₂)) = fl₁fl₂⊆fl₂ k v' k,v'∈fl₁l₂
-                            k∈kf'l₂ = updating-via-∈k-forward (f l₂) ks (updater l₂) (forget {m = f l₂} k,v''∈fl₂)
+                            k∈kf'l₂ = updating-via-∈k-forward (f l₂) ks (updater l₂) (forget k,v''∈fl₂)
                         in
                             ⊥-elim (k∉kf'l₂ k∈kf'l₂)
                 ...   | in₂ k∉kf'l₁ (single k,v'∈f'l₂) =
@@ -1074,10 +1046,10 @@ module _ {l} {L : Set l}
 
                 f'l₂⊆f'l₁f'l₂ : f' l₂ ⊆ ((f' l₁) ⊔ (f' l₂))
                 f'l₂⊆f'l₁f'l₂ k v k,v∈f'l₂
-                    with k∈kfl₂ ← updating-via-∈k-backward (f l₂) ks (updater l₂) (forget {m = f' l₂} k,v∈f'l₂)
+                    with k∈kfl₂ ← updating-via-∈k-backward (f l₂) ks (updater l₂) (forget k,v∈f'l₂)
                     with (v' , k,v'∈fl₂) ← locate {m = f l₂} k∈kfl₂
                     with (v'' , (v'≈v'' , k,v''∈fl₁fl₂)) ← fl₂⊆fl₁fl₂ k v' k,v'∈fl₂
-                    with Expr-Provenance-≡ k v'' ((` (f l₁)) ∪ (` (f l₂))) k,v''∈fl₁fl₂
+                    with Expr-Provenance-≡ ((` (f l₁)) ∪ (` (f l₂))) k,v''∈fl₁fl₂
                 ...   | in₁ (single k,v''∈fl₁) k∉kfl₂ = ⊥-elim (k∉kfl₂ k∈kfl₂)
                 ...   | in₂ k∉kfl₁ (single k,v''∈fl₂) =
                         let
@@ -1088,8 +1060,8 @@ module _ {l} {L : Set l}
                         with k∈-dec k ks
                 ...       | yes k∈ks with refl ← updating-via-k∈ks-≡ (f l₂) (updater l₂) k∈ks k,v∈f'l₂ =
                             let
-                                k,uv₁∈f'l₁ = updating-via-k∈ks-forward (f l₁) (updater l₁) k∈ks (forget {m = f l₁} k,v₁∈fl₁)
+                                k,uv₁∈f'l₁ = updating-via-k∈ks-forward (f l₁) (updater l₁) k∈ks (forget k,v₁∈fl₁)
-                                k,uv₂∈f'l₂ = updating-via-k∈ks-forward (f l₂) (updater l₂) k∈ks (forget {m = f l₂} k,v₂∈fl₂)
+                                k,uv₂∈f'l₂ = updating-via-k∈ks-forward (f l₂) (updater l₂) k∈ks (forget k,v₂∈fl₂)
                                 k,uv₁uv₂∈f'l₁f'l₂ = ⊔-combines {m₁ = f' l₁} {m₂ = f' l₂} k,uv₁∈f'l₁ k,uv₂∈f'l₂
                             in
                                 (updater l₁ k ⊔₂ updater l₂ k , (IsLattice.≈-sym lB (g-Monotonicʳ k l₁≼l₂) , k,uv₁uv₂∈f'l₁f'l₂))

Utils.agda

@@ -1,5 +1,6 @@
 module Utils where
 
+open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
 open import Data.Nat using (ℕ; suc)
 open import Data.List using (List; []; _∷_; _++_)
 open import Data.List.Membership.Propositional using (_∈_)
@@ -43,3 +44,9 @@ All-x∈xs (x ∷ xs') = here refl ∷ map there (All-x∈xs xs')
 iterate : ∀ {a} {A : Set a} (n : ℕ) → (f : A → A) → A → A
 iterate 0 _ a = a
 iterate (suc n) f a = f (iterate n f a)
+
+data Pairwise {a} {b} {c} {A : Set a} {B : Set b} (P : A → B → Set c) : List A → List B → Set (a ⊔ℓ b ⊔ℓ c)  where
+    [] : Pairwise P [] []
+    _∷_ : ∀ {x : A} {y : B} {xs : List A} {ys : List B} →
+          P x y → Pairwise P xs ys →
+          Pairwise P (x ∷ xs) (y ∷ ys)