diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 435c788c7b41aa6a986a361f78ddf93ab11d67f0..47f9ece52feef180e593874b4a282ee5629f7b4b 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -284,7 +284,7 @@ Section fupd_derived.
     ((|={E2,E1}=> emp) ={E2,E3}=∗ P) -∗ |={E1,E3}=> P.
   Proof.
     intros HE.
-    (* Get an [emp] so we can apply [fupd_intro_mask']. *)
+    (* Get an [emp] so we can apply [fupd_mask_subseteq]. *)
     rewrite -[X in (X -∗ _)](left_id emp%I bi_sep).
     rewrite {1}(fupd_mask_subseteq E2) //.
     rewrite fupd_frame_r. by rewrite wand_elim_r fupd_trans.