diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2207c555923af5c1ffcad21e2eb1dbcdcfa24046..2cbbeaca0038098b74daca218e90ff24eacd3f4e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -111,6 +111,8 @@ API-breaking change is listed.
 - Make `done` work on goals of the form `is_Some`.
 - Add `mk_evar` tactic to generate evars (intended as a more useful replacement
   for Coq's `evar` tactic).
+- Make `solve_ndisj` able to solve more goals of the form `_ âŠ† âŠ¤ âˆ– _`,
+  `_ âˆ– _ ## _`, `_ ## _ âˆ– _`, as well as `_ ## âˆ…` and `âˆ… ## _`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/tests/solve_ndisj.v b/tests/solve_ndisj.v
index 3774753969a307d0d8196c80d6c094c64f82b544..09ec793416c260a163cb75646320e1babb9d8e45 100644
--- a/tests/solve_ndisj.v
+++ b/tests/solve_ndisj.v
@@ -1,21 +1,32 @@
 From stdpp Require Import namespaces strings.
 
-Lemma test1 (N1 N2 : namespace) :
+Section tests.
+Implicit Types (N : namespace) (E : coPset).
+
+Lemma test1 N1 N2 :
   N1 ## N2 â†’ â†‘N1 âŠ†@{coPset} âŠ¤ âˆ– â†‘N2.
 Proof. solve_ndisj. Qed.
 
-Lemma test2 (N1 N2 : namespace) :
+Lemma test2 N1 N2 :
   N1 ## N2 â†’ â†‘N1.@"x" âŠ†@{coPset} âŠ¤ âˆ– â†‘N1.@"y" âˆ– â†‘N2.
 Proof. solve_ndisj. Qed.
 
-Lemma test3 (N : namespace) :
+Lemma test3 N :
   âŠ¤ âˆ– â†‘N âŠ†@{coPset} âŠ¤ âˆ– â†‘N.@"x".
 Proof. solve_ndisj. Qed.
 
-Lemma test4 (N : namespace) :
+Lemma test4 N :
   âŠ¤ âˆ– â†‘N âŠ†@{coPset} âŠ¤ âˆ– â†‘N.@"x" âˆ– â†‘N.@"y".
 Proof. solve_ndisj. Qed.
 
-Lemma test5 (N1 N2 : namespace) :
+Lemma test5 N1 N2 :
   âŠ¤ âˆ– â†‘N1 âˆ– â†‘N2 âŠ†@{coPset} âŠ¤ âˆ– â†‘N1.@"x" âˆ– â†‘N2 âˆ– â†‘N1.@"y".
 Proof. solve_ndisj. Qed.
+
+Lemma test6 E N :
+  â†‘N âŠ† E â†’ â†‘N âŠ† âŠ¤ âˆ– (E âˆ– â†‘N).
+Proof. solve_ndisj. Qed.
+
+Lemma test7 N :
+  â†‘N âŠ†@{coPset} âŠ¤ âˆ– âˆ….
+Proof. solve_ndisj. Qed.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index 7065e423dedebffe10685a4c8776b6a4ac53c25d..b2e15d73d1bbf9abb71b73ef4e16ae4d4334cc81 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -99,6 +99,17 @@ Global Hint Resolve coPset_disjoint_difference_l1 | 50 : ndisj.
 Local Definition coPset_disjoint_difference_l2 := disjoint_difference_l2 (C:=coPset).
 Global Hint Resolve coPset_disjoint_difference_l2 | 100 : ndisj.
 Global Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r | 100 : ndisj.
+Local Definition coPset_disjoint_empty_l := disjoint_empty_l (C:=coPset).
+Global Hint Resolve coPset_disjoint_empty_l : ndisj.
+Local Definition coPset_disjoint_empty_r := disjoint_empty_r (C:=coPset).
+Global Hint Resolve coPset_disjoint_empty_r : ndisj.
+(** We prefer âˆ– on the left of ## (for the [disjoint_difference] lemmas to
+apply), so try moving it there. *)
+Global Hint Extern 10 (_ ## (_ âˆ– _)) =>
+  lazymatch goal with
+  | |- (_ âˆ– _) ## _ => fail (* âˆ– on both sides, leave it be *)
+  | |- _ => symmetry
+  end : ndisj.
 
 Ltac solve_ndisj :=
   repeat match goal with