diff --git a/modures/excl.v b/modures/excl.v
index 795c2840d1b42fcae5f20fbad07c8f8fb84a71af..341e7b27ac23441f36578d4a648cbe6f35caecfe 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -142,6 +142,8 @@ Qed.
 (* Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ⇝ y.
 Proof. by destruct y; intros ? [?| |]. Qed.
+Lemma excl_updateP (P : excl A → Prop) x y : ✓ y → P y → Excl x ⇝: P.
+Proof. intros ?? z n ?; exists y. by destruct y, z as [?| |]. Qed.
 End excl.
 
 Arguments exclC : clear implicits.