diff --git a/modures/excl.v b/modures/excl.v
index c3367fccf28e58490f915d2e24f4f08f8d34fc1d..6382906841af3c652d47c7920414d1888e6e7840 100644
--- a/modures/excl.v
+++ b/modures/excl.v
@@ -127,6 +127,10 @@ Proof.
 Qed.
 Canonical Structure exclRA : cmraT :=
   CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
+Lemma excl_validN_inv_l n x y : ✓{S n} (Excl x ⋅ y) → y = ∅.
+Proof. by destruct y. Qed.
+Lemma excl_validN_inv_r n x y : ✓{S n} (x ⋅ Excl y) → x = ∅.
+Proof. by destruct x. Qed.
 
 (* Updates *)
 Lemma excl_update (x : A) y : ✓ y → Excl x ⇝ y.