diff --git a/tests/solve_ndisj.v b/tests/solve_ndisj.v
index fee607f8ac991992c64fb3828008d8826d112bc5..fe6aebdb361fabaa0e2cc52c5bea1a262e8b63cc 100644
--- a/tests/solve_ndisj.v
+++ b/tests/solve_ndisj.v
@@ -35,3 +35,11 @@ Proof. solve_ndisj. Qed.
 Lemma test7 N :
   ↑N ⊆@{coPset} ⊤ ∖ ∅.
 Proof. solve_ndisj. Qed.
+
+Lemma test8 N1 N2 :
+  ⊤ ∖ (↑N1 ∪ ↑N2) ⊆@{coPset} ⊤ ∖ ↑N1.@"counter".
+Proof. solve_ndisj. Qed.
+
+Lemma test9 N1 N2 :
+  ⊤ ∖ (↑N1 ∪ ↑N2) ⊆@{coPset} ⊤ ∖ ↑N1.@"counter" ∖ ↑N1.@"state" ∖ ↑N2.
+Proof. solve_ndisj. Qed.
diff --git a/theories/namespaces.v b/theories/namespaces.v
index b2e15d73d1bbf9abb71b73ef4e16ae4d4334cc81..094afabc818ee2cedd4f09e9f4a6ee4f24f22828 100644
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
@@ -84,6 +84,11 @@ Local Definition coPset_empty_subseteq := empty_subseteq (C:=coPset).
 Global Hint Resolve coPset_empty_subseteq : ndisj.
 Local Definition coPset_union_least := union_least (C:=coPset).
 Global Hint Resolve coPset_union_least : ndisj.
+(** For goals like [X ⊆ L ∪ R], backtrack for the two sides. *)
+Local Definition coPset_union_subseteq_l' := union_subseteq_l' (C:=coPset).
+Global Hint Resolve coPset_union_subseteq_l' | 50 : ndisj.
+Local Definition coPset_union_subseteq_r' := union_subseteq_r' (C:=coPset).
+Global Hint Resolve coPset_union_subseteq_r' | 50 : ndisj.
 (** Fallback, loses lots of information but lets other rules make progress. *)
 Local Definition coPset_subseteq_difference_l := subseteq_difference_l (C:=coPset).
 Global Hint Resolve coPset_subseteq_difference_l | 100 : ndisj.
diff --git a/theories/sets.v b/theories/sets.v
index 0d892c9fa23c46a43ad07902f6762f0df971821d..3bfef5767e66bccb606ff35e966635bb6b47d8fd 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -385,8 +385,12 @@ Section semi_set.
 
   Lemma union_subseteq_l X Y : X ⊆ X ∪ Y.
   Proof. set_solver. Qed.
+  Lemma union_subseteq_l' X X' Y : X ⊆ X' → X ⊆ X' ∪ Y.
+  Proof. set_solver. Qed.
   Lemma union_subseteq_r X Y : Y ⊆ X ∪ Y.
   Proof. set_solver. Qed.
+  Lemma union_subseteq_r' X Y Y' : Y ⊆ Y' → Y ⊆ X ∪ Y'.
+  Proof. set_solver. Qed.
   Lemma union_least X Y Z : X ⊆ Z → Y ⊆ Z → X ∪ Y ⊆ Z.
   Proof. set_solver. Qed.