diff --git a/Lattice/Map.agda b/Lattice/Map.agda
index 88e82aa..d6731aa 100644
--- a/Lattice/Map.agda
+++ b/Lattice/Map.agda
@@ -28,8 +28,9 @@ open IsLattice lB using () renaming
     ; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
     )
 
-keys : List (A × B) → List A
-keys = map proj₁
+module ImplKeys where
+    keys : List (A × B) → List A
+    keys = map proj₁
 
 data Unique {c} {C : Set c} : List C → Set c where
     empty : Unique []
@@ -57,6 +58,7 @@ All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
 
 private module _ where
     open MemProp using (_∈_)
+    open ImplKeys
 
     unique-not-in : ∀ {k : A} {v : B} {l : List (A × B)}  →
                     ¬ (All (λ k' → ¬ k ≡ k') (keys l) × (k , v) ∈ l)
@@ -108,6 +110,7 @@ private module ImplRelation where
 private module ImplInsert (f : B → B → B) where
     open import Data.List using (map)
     open MemProp using (_∈_)
+    open ImplKeys
 
     private
         _∈k_ : A → List (A × B) → Set a
@@ -448,13 +451,16 @@ private module ImplInsert (f : B → B → B) where
 
 
 Map : Set (a ⊔ℓ b)
-Map = Σ (List (A × B)) (λ l → Unique (keys l))
+Map = Σ (List (A × B)) (λ l → Unique (ImplKeys.keys l))
+
+keys : Map → List A
+keys (kvs , _) = ImplKeys.keys kvs
 
 _∈_ : (A × B) → Map → Set (a ⊔ℓ b)
 _∈_ p (kvs , _) = MemProp._∈_ p kvs
 
 _∈k_ : A → Map → Set a
-_∈k_ k (kvs , _) = MemProp._∈_ k (keys kvs)
+_∈k_ k m = MemProp._∈_ k (keys m)
 
 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