diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda
index 42ed8ad..672976b 100644
--- a/Analysis/Sign.agda
+++ b/Analysis/Sign.agda
@@ -204,7 +204,7 @@ module _ (prog : Program) where
             in
                 vs updatingᵛ (k ∷ []) via (λ _ → eval e k∈e⇒k∈vars vs)
 
-    open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateForState {!!} states
+    open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ joinAll (λ {a₁} {a₂} a₁≼a₂ → joinAll-Mono {a₁} {a₂} a₁≼a₂) updateForState {!!} states
         renaming
             ( f' to updateAll
             ; f'-Monotonic to updateAll-Mono