diff --git a/algebra/excl.v b/algebra/excl.v
index cf50b1f71d1157a80e92c13fa4d262002a7beb94..e7023685ca3bfc3977fe76f98d3d1c9cfe8a3bf9 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -143,6 +143,10 @@ Global Instance excl_local_update b :
   LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, Excl b).
 Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.
 
+Global Instance excl_local_update_del :
+LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, ExclUnit).
+Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.
+
 (** Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ~~> y.
 Proof. by destruct y; intros ? [?| |]. Qed.