From e1e5349adae403109ed9891c88adfd3abe7c8e83 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 18 Jun 2018 18:52:25 +0200
Subject: [PATCH] generalize ndisj_subseteq_difference to work for all masks

---
 theories/namespaces.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/namespaces.v b/theories/namespaces.v
index 6828bfc0..78d2bedf 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -73,7 +73,8 @@ Section namespace.
   Lemma ndot_preserve_disjoint_r N E x : E ## â†‘N â†’ E ## â†‘N.@x.
   Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
 
-  Lemma ndisj_subseteq_difference N E F : E ## â†‘N â†’ E âŠ† F â†’ E âŠ† F âˆ– â†‘N.
+  Lemma namespace_subseteq_difference E1 E2 E3 :
+    E1 ## E3 â†’ E1 âŠ† E2 â†’ E1 âŠ† E2 âˆ– E3.
   Proof. set_solver. Qed.
 
   Lemma namespace_subseteq_difference_l E1 E2 E3 : E1 âŠ† E3 â†’ E1 âˆ– E2 âŠ† E3.
@@ -89,7 +90,7 @@ of the forms:
 - [â†‘N1 âŠ† E âˆ– â†‘N2 âˆ– .. âˆ– â†‘Nn]
 - [E1 âˆ– â†‘N1 âŠ† E2 âˆ– â†‘N2 âˆ– .. âˆ– â†‘Nn] *)
 Create HintDb ndisj.
-Hint Resolve ndisj_subseteq_difference : ndisj.
+Hint Resolve namespace_subseteq_difference : ndisj.
 Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
 Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r : ndisj.
 Hint Resolve nclose_subseteq' ndisj_difference_l : ndisj.
-- 
GitLab