diff --git a/Lattice/Map.agda b/Lattice/Map.agda
index f5c8c33..405a7d3 100644
--- a/Lattice/Map.agda
+++ b/Lattice/Map.agda
@@ -19,7 +19,7 @@ open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-ex
 open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Equivalence
-open import Utils using (Unique; push; empty; Unique-append; All¬-¬Any; All-x∈xs)
+open import Utils using (Unique; push; Unique-append; All¬-¬Any; All-x∈xs)
 
 open IsLattice lB using () renaming
     ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
@@ -34,6 +34,21 @@ private module ImplKeys where
     keys : List (A × B) → List A
     keys = map proj₁
 
+-- See note on `forget` for why this is defined in global scope even though
+-- it operates on lists.
+∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ˡ (ImplKeys.keys l))
+∈k-dec k [] = no (λ ())
+∈k-dec k ((k' , v) ∷ xs)
+    with (≡-dec-A k k')
+...   | yes k≡k' = yes (here k≡k')
+...   | no k≢k' with (∈k-dec k xs)
+...       | yes k∈kxs = yes (there k∈kxs)
+...       | no k∉kxs = no witness
+              where
+                  witness : ¬ k ∈ˡ (ImplKeys.keys ((k' , v) ∷ xs))
+                  witness (here k≡k') = k≢k' k≡k'
+                  witness (there k∈kxs) = k∉kxs k∈kxs
+
 private module _ where
     open MemProp using (_∈_)
     open ImplKeys
@@ -65,19 +80,6 @@ private module _ where
     ...       | yes k∈xs = yes (there k∈xs)
     ...       | no k∉xs = no (λ { (here k≡x) → k≢x k≡x; (there k∈xs) → k∉xs k∈xs })
 
-    ∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ keys l)
-    ∈k-dec k [] = no (λ ())
-    ∈k-dec k ((k' , v) ∷ xs)
-        with (≡-dec-A k k')
-    ...   | yes k≡k' = yes (here k≡k')
-    ...   | no k≢k' with (∈k-dec k xs)
-    ...       | yes k∈kxs = yes (there k∈kxs)
-    ...       | no k∉kxs = no witness
-                  where
-                      witness : ¬ k ∈ keys ((k' , v) ∷ xs)
-                      witness (here k≡k') = k≢k' k≡k'
-                      witness (there k∈kxs) = k∉kxs k∈kxs
-
     ∈-cong : ∀ {c d} {C : Set c} {D : Set d} {c : C} {l : List C} →
              (f : C → D) → c ∈ l → f c ∈ map f l
     ∈-cong f (here c≡c') = here (cong f c≡c')
@@ -340,7 +342,7 @@ private module ImplInsert (f : B → B → B) where
 
     restrict-preserves-Unique : ∀ {l₁ l₂ : List (A × B)} →
                                 Unique (keys l₂) → Unique (keys (restrict l₁ l₂))
-    restrict-preserves-Unique {l₁} {[]} _ = empty
+    restrict-preserves-Unique {l₁} {[]} _ = Utils.empty
     restrict-preserves-Unique {l₁} {(k , v) ∷ xs} (push k≢xs uxs)
         with ∈k-dec k l₁
     ...   | yes _ = push (restrict-preserves-k≢ k≢xs) (restrict-preserves-Unique uxs)
@@ -476,6 +478,9 @@ private module ImplInsert (f : B → B → B) where
 Map : Set (a ⊔ℓ b)
 Map = Σ (List (A × B)) (λ l → Unique (ImplKeys.keys l))
 
+empty : Map
+empty = ([] , Utils.empty)
+
 keys : Map → List A
 keys (kvs , _) = ImplKeys.keys kvs
 
@@ -488,8 +493,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
 
--- 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` and `∈k-dec` are 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₁
 
@@ -529,9 +535,12 @@ data Expr : Set (a ⊔ℓ b) where
     _∪_ : Expr → Expr → Expr
     _∩_ : Expr → Expr → Expr
 
-open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys) renaming (insert to insert-impl; union to union-impl)
+open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys; insert-preserves-Unique) renaming (insert to insert-impl; union to union-impl)
 open ImplInsert _⊓₂_ using (intersect-preserves-Unique; intersect-equal-keys) renaming (intersect to intersect-impl)
 
+insert : A → B → Map → Map
+insert k v (l , uks) = (insert-impl k v l , insert-preserves-Unique uks)
+
 _⊔_ : Map → Map → Map
 _⊔_ (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂)
 
@@ -878,6 +887,8 @@ isLattice = record
     ; absorb-⊓-⊔ = absorb-⊓-⊔
     }
 
+open IsLattice isLattice using (_≼_) public
+
 lattice : Lattice Map
 lattice = record
     { _≈_ = _≈_
@@ -958,6 +969,10 @@ _updating_via_ (kvs , uks) ks f =
     , subst Unique (transform-keys-≡ kvs ks f) uks
     )
 
+updating-via-keys-≡ : ∀ (m : Map) (ks : List A) (f : A → B) →
+                  keys m ≡ keys (m updating ks via f)
+updating-via-keys-≡ (l , _) = transform-keys-≡ l
+
 updating-via-∉k-forward : ∀ (m : Map) (ks : List A) (f : A → B) {k : A} →
                           ¬ k ∈k m → ¬ k ∈k (m updating ks via f)
 updating-via-∉k-forward m = transform-∉k-forward
@@ -995,7 +1010,6 @@ updating-via-k∉ks-backward m = transform-k∉ks-backward
 module _ {l} {L : Set l}
          {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
          (lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where
-    open IsLattice isLattice using (_≼_)
     open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
 
     module _ (f : L → Map) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)