diff --git a/iris/algebra/local_updates.v b/iris/algebra/local_updates.v
index dd679d26ff1cade494e850a338e354a670b714e5..c8a854745757ddfb77018b9a026f62a2870355c6 100644
--- a/iris/algebra/local_updates.v
+++ b/iris/algebra/local_updates.v
@@ -200,3 +200,10 @@ Proof.
   move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
   eapply cmra_validN_le; [|lia]. eapply Hy.
 Qed.
+
+Lemma delete_option_local_update_cancelable {A : cmra} (mx : option A) :
+  Cancelable mx → (mx, mx) ~l~> (None, None).
+Proof.
+  intros ?. apply local_update_unital=>n mf /= Hmx Heq. split; first done.
+  rewrite left_id. eapply (cancelableN mx); by rewrite right_id_L.
+Qed.