diff --git a/Lattice/FiniteMap.agda b/Lattice/FiniteMap.agda
index 76f9722..aa45fc1 100644
--- a/Lattice/FiniteMap.agda
+++ b/Lattice/FiniteMap.agda
@@ -38,6 +38,8 @@ open import Lattice.Map ≡-dec-A lB as Map
         ; 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
+        ; updating-via-k∉ks-forward to updatingᵐ-via-k∉ks-forward
+        ; updating-via-k∉ks-backward to updatingᵐ-via-k∉ks-backward
         ; f'-Monotonic to f'-Monotonicᵐ
         ; _≼_ to _≼ᵐ_
         ; ∈k-dec to ∈k-decᵐ
@@ -185,6 +187,12 @@ module WithKeys (ks : List A) where
         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)
 
+        f'-k∉ks-forward : ∀ {k v l} → ¬ k ∈ˡ ks → (k , v) ∈ (f l) → (k , v) ∈ (f' l)
+        f'-k∉ks-forward {k} {v} {l} = updatingᵐ-via-k∉ks-forward (proj₁ (f l)) (updater l)
+
+        f'-k∉ks-backward : ∀ {k v l} → ¬ k ∈ˡ ks → (k , v) ∈ (f' l) → (k , v) ∈ (f l)
+        f'-k∉ks-backward {k} {v} {l} = updatingᵐ-via-k∉ks-backward (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)