diff --git a/iris/algebra/local_updates.v b/iris/algebra/local_updates.v
index 6eb0a090cacf876cf78ad167db720d5744f318f2..87a436473cd8eb8e60e68e30675182a0cb74d346 100644
--- a/iris/algebra/local_updates.v
+++ b/iris/algebra/local_updates.v
@@ -154,7 +154,7 @@ Proof.
     eapply Hupd, Hg; eauto.
   - specialize (Hupd i).
     rewrite local_update_unital in Hupd.
-    eapply Hupd; eauto.
+    eapply Hupd, Hg; eauto.
 Qed.
 
 (** * Product *)