diff --git a/Lattice/Map.agda b/Lattice/Map.agda
index 3bf8c28..b1d2e61 100644
--- a/Lattice/Map.agda
+++ b/Lattice/Map.agda
@@ -73,9 +73,9 @@ private module _ where
     ∈-cong f (here c≡c') = here (cong f c≡c')
     ∈-cong f (there c∈xs) = there (∈-cong f c∈xs)
 
-    locate : ∀ {k : A} {l : List (A × B)} → k ∈ keys l → Σ B (λ v → (k , v) ∈ l)
-    locate {k} {(k' , v) ∷ xs} (here k≡k') rewrite k≡k' = (v , here refl)
-    locate {k} {(k' , v) ∷ xs} (there k∈kxs) = let (v , k,v∈xs) = locate k∈kxs in (v , there k,v∈xs)
+    locate-impl : ∀ {k : A} {l : List (A × B)} → k ∈ keys l → Σ B (λ v → (k , v) ∈ l)
+    locate-impl {k} {(k' , v) ∷ xs} (here k≡k') rewrite k≡k' = (v , here refl)
+    locate-impl {k} {(k' , v) ∷ xs} (there k∈kxs) = let (v , k,v∈xs) = locate-impl k∈kxs in (v , there k,v∈xs)
 
 private module ImplRelation where
     open MemProp using (_∈_)
@@ -476,6 +476,12 @@ _∈_ p (kvs , _) = MemProp._∈_ p kvs
 _∈k_ : A → Map → Set a
 _∈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
+forget = ∈-cong proj₁
+
 Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v'
 Map-functional {m = (l , ul)} k,v∈m k,v'∈m = ListAB-functional ul k,v∈m k,v'∈m
 
@@ -549,7 +555,7 @@ data Provenance (k : A) : B → Expr → Set (a ⊔ℓ b) where
     bothⁱ : ∀ {v₁ v₂ : B} {e₁ e₂ : Expr} → Provenance k v₁ e₁ → Provenance k v₂ e₂ → Provenance k (v₁ ⊓₂ v₂) (e₁ ∩ e₂)
 
 Expr-Provenance : ∀ (k : A) (e : Expr) → k ∈k ⟦ e ⟧ → Σ B (λ v → (Provenance k v e × (k , v) ∈ ⟦ e ⟧))
-Expr-Provenance k (` m) k∈km = let (v , k,v∈m) = locate k∈km in (v , (single k,v∈m , k,v∈m))
+Expr-Provenance k (` m) k∈km = let (v , k,v∈m) = locate-impl k∈km in (v , (single k,v∈m , k,v∈m))
 Expr-Provenance k (e₁ ∪ e₂) k∈ke₁e₂
     with ∈k-dec k (proj₁ ⟦ e₁ ⟧) | ∈k-dec k (proj₁ ⟦ e₂ ⟧)
 ...   | yes k∈ke₁ | yes k∈ke₂ =
@@ -582,7 +588,7 @@ module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where
 
         SubsetInfo-to-dec : ∀ {m₁ m₂ : Map} → SubsetInfo m₁ m₂ → Dec (m₁ ⊆ m₂)
         SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) =
-            let (v , k,v∈m₁) = locate k∈km₁
+            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₂))
@@ -601,7 +607,7 @@ module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where
                 mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂
         ...   | fine xs₁⊆m₂ with ∈k-dec k l₂
         ...       | no k∉km₂ = extra k (here refl) k∉km₂
-        ...       | yes k∈km₂ with locate k∈km₂
+        ...       | yes k∈km₂ with locate-impl k∈km₂
         ...           | (v' , k,v'∈m₂) with ≈₂-dec v v'
         ...               | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v'
         ...               | yes v≈v' = fine m₁⊆m₂
@@ -635,7 +641,7 @@ private module I⊓ = ImplInsert _⊓₂_
     where
         ≈-∉-cong : ∀ {m₁ m₂ : Map} {k : A} → m₁ ≈ m₂ → ¬ k ∈k m₁ → ¬ k ∈k m₂
         ≈-∉-cong (m₁⊆m₂ , m₂⊆m₁) k∉km₁ k∈km₂ =
-            let (v₂ , k,v₂∈m₂) = locate k∈km₂
+            let (v₂ , k,v₂∈m₂) = locate-impl k∈km₂
                 (_ , (_ , k,v₁∈m₁)) = m₂⊆m₁ _ v₂ k,v₂∈m₂
             in k∉km₁ (∈-cong proj₁ k,v₁∈m₁)
 
@@ -825,7 +831,7 @@ absorb-⊓-⊔ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊓-⊔¹ , absor
         absorb-⊓-⊔² k v k,v∈m₁
             with ∈k-dec k l₂
         ...   | yes k∈km₂ =
-                let (v₂ , k,v₂∈m₂) = locate k∈km₂
+                let (v₂ , k,v₂∈m₂) = locate-impl k∈km₂
                 in (v ⊓₂ (v ⊔₂ v₂) , (≈₂-sym (absorb-⊓₂-⊔₂ v v₂) , I⊓.intersect-combines u₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) k,v∈m₁ (I⊔.union-combines u₁ u₂ k,v∈m₁ k,v₂∈m₂)))
         ...   | no k∉km₂ = (v ⊓₂ v , (≈₂-sym (⊓₂-idemp v) , I⊓.intersect-combines u₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) k,v∈m₁ (I⊔.union-preserves-∈₁ u₁ k,v∈m₁ k∉km₂)))
 
@@ -852,7 +858,7 @@ absorb-⊔-⊓ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊔-⊓¹ , absor
         absorb-⊔-⊓² k v k,v∈m₁
             with ∈k-dec k l₂
         ...   | yes k∈km₂ =
-                let (v₂ , k,v₂∈m₂) = locate k∈km₂
+                let (v₂ , k,v₂∈m₂) = locate-impl k∈km₂
                 in (v ⊔₂ (v ⊓₂ v₂) , (≈₂-sym (absorb-⊔₂-⊓₂ v v₂) , I⊔.union-combines u₁ (I⊓.intersect-preserves-Unique {l₁} {l₂} u₂) k,v∈m₁ (I⊓.intersect-combines u₁ u₂ k,v∈m₁ k,v₂∈m₂)))
         ...   | no k∉km₂ = (v , (≈₂-refl , I⊔.union-preserves-∈₁ u₁ k,v∈m₁ (I⊓.intersect-preserves-∉₂ {k} {l₁} {l₂} k∉km₂)))