diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda
index ca4cb7c..76f9722 100644
--- a/Lattice/FiniteMap.agda
+++ b/Lattice/FiniteMap.agda
@@ -35,6 +35,9 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; keys to keysᵐ
         ; _updating_via_ to _updatingᵐ_via_
         ; updating-via-keys-≡ to updatingᵐ-via-keys-≡
+        ; updating-via-k∈ks to updatingᵐ-via-k∈ks
+        ; updating-via-k∈ks-≡ to updatingᵐ-via-k∈ks-≡
+        ; updating-via-∈k-forward to updatingᵐ-via-∈k-forward
         ; f'-Monotonic to f'-Monotonicᵐ
         ; _≼_ to _≼ᵐ_
         ; ∈k-dec to ∈k-decᵐ
@@ -83,6 +86,8 @@ module WithKeys (ks : List A) where
     _∈k_ : A → FiniteMap → Set a
     _∈k_ k (m₁ , _) = k ∈ˡ (keysᵐ m₁)
 
+    open Map using (forget) public
+
     ∈k-dec = ∈k-decᵐ
 
     locate : ∀ {k : A} {fm : FiniteMap} → k ∈k fm → Σ B (λ v → (k , v) ∈ fm)
@@ -171,6 +176,15 @@ module WithKeys (ks : List A) where
         f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
         f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
 
+        f'-∈k-forward : ∀ {k l} → k ∈k (f l) → k ∈k (f' l)
+        f'-∈k-forward {k} {l} = updatingᵐ-via-∈k-forward (proj₁ (f l)) ks (updater l)
+
+        f'-k∈ks : ∀ {k l} → k ∈ˡ ks → k ∈k (f' l) → (k , updater l k) ∈ (f' l)
+        f'-k∈ks {k} {l} = updatingᵐ-via-k∈ks (proj₁ (f l)) (updater l)
+
+        f'-k∈ks-≡ : ∀ {k v l} → k ∈ˡ ks → (k , v) ∈ (f' l) → v ≡ updater l k
+        f'-k∈ks-≡ {k} {v} {l} = updatingᵐ-via-k∈ks-≡ (proj₁ (f l)) (updater l)
+
     all-equal-keys : ∀ (fm₁ fm₂ : FiniteMap) → (Map.keys (proj₁ fm₁) ≡ Map.keys (proj₁ fm₂))
     all-equal-keys (fm₁ , km₁≡ks) (fm₂ , km₂≡ks) = trans km₁≡ks (sym km₂≡ks)
 
diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda
index c4c3c3c..47c6104 100644
--- a/Lattice/FiniteValueMap.agda
+++ b/Lattice/FiniteValueMap.agda
@@ -32,7 +32,7 @@ open import Isomorphism using (IsInverseˡ; IsInverseʳ)
 open import Lattice.Map ≡-dec-A lB
     using
         ( subset-impl
-        ; locate; forget
+        ; locate
         ; Map-functional
         ; Expr-Provenance
         ; Expr-Provenance-≡