diff --git a/base_logic/lib/namespaces.v b/base_logic/lib/namespaces.v
index 35e0c148e421e529f118a1bdebb03148201348e7..549ecf193943bddb8bee3663ba169b3475df52dd 100644
--- a/base_logic/lib/namespaces.v
+++ b/base_logic/lib/namespaces.v
@@ -73,14 +73,25 @@ Section namespace.
 
   Lemma ndisj_subseteq_difference N E F : E âŠ¥ â†‘N â†’ E âŠ† F â†’ E âŠ† F âˆ– â†‘N.
   Proof. set_solver. Qed.
+
+  Lemma namespace_subseteq_difference_l E1 E2 E3 : E1 âŠ† E3 â†’ E1 âˆ– E2 âŠ† E3.
+  Proof. set_solver. Qed.
+
+  Lemma ndisj_difference_l E N1 N2 : â†‘N2 âŠ† (â†‘N1 : coPset) â†’ E âˆ– â†‘N1 âŠ¥ â†‘N2.
+  Proof. set_solver. Qed.
 End namespace.
 
 (* The hope is that registering these will suffice to solve most goals
-of the form [N1 âŠ¥ N2] and those of the form [â†‘N1 âŠ† E âˆ– â†‘N2 âˆ– .. âˆ– â†‘Nn]. *)
+of the forms:
+- [N1 âŠ¥ N2] 
+- [â†‘N1 âŠ† E âˆ– â†‘N2 âˆ– .. âˆ– â†‘Nn]
+- [E1 âˆ– â†‘N1 âŠ† E2 âˆ– â†‘N2 âˆ– .. âˆ– â†‘Nn] *)
 Hint Resolve ndisj_subseteq_difference : ndisj.
 Hint Extern 0 (_ âŠ¥ _) => apply ndot_ne_disjoint; congruence : ndisj.
 Hint Resolve ndot_preserve_disjoint_l : ndisj.
 Hint Resolve ndot_preserve_disjoint_r : ndisj.
 Hint Extern 1 (_ âŠ† _) => apply nclose_subseteq' : ndisj.
+Hint Resolve 100 namespace_subseteq_difference_l : ndisj.
+Hint Resolve ndisj_difference_l : ndisj.
 
 Ltac solve_ndisj := solve [eauto with ndisj].