diff --git a/algebra/excl.v b/algebra/excl.v
index 5e83c0e59a44fa3aa049249d3be553ea23cd5699..c67a912fabbcc6157369e752d167074cb2f36c61 100644
--- a/algebra/excl.v
+++ b/algebra/excl.v
@@ -116,7 +116,7 @@ Proof. uPred.unseal. by destruct x. Qed.
 
 (** ** Local updates *)
 Global Instance excl_local_update y :
-  LocalUpdate (λ x, if x is Excl _ then ✓ y else False) (λ _, y).
+  LocalUpdate (λ _, True) (λ _, y).
 Proof. split. apply _. by destruct y; intros n [a|] [b'|]. Qed.
 
 (** Updates *)