diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 7ea069d64d7b0e2c1e98c940acb1532afd354d80..cdb86b1aa7cee674b23d0601c3badb53b996aa44 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -166,9 +166,8 @@ Proof.
   destruct z as [z|]; last done. destruct y; inversion Heq.
 Qed.
 
-Lemma delete_option_local_update {A : cmraT} (x y : A) :
-  Exclusive y →
-  (Some x, Some y) ~l~> (None, None).
+Lemma delete_option_local_update {A : cmraT} (x : option A) (y : A) :
+  Exclusive y → (x, Some y) ~l~> (None, None).
 Proof.
   move=>Hex. apply local_update_unital=>n z /= Hy Heq. split; first done.
   destruct z as [z|]; last done. exfalso.