diff --git a/tests/fin_maps.v b/tests/fin_maps.v
index 842c20a80d908673e12a5e5e11a4460ce2f77db6..b81d06aeb5b249326e07af3130c6d2a8c058dd02 100644
--- a/tests/fin_maps.v
+++ b/tests/fin_maps.v
@@ -1,4 +1,4 @@
-From stdpp Require Import fin_maps.
+From stdpp Require Import fin_maps fin_map_dom.
 
 Section map_disjoint.
   Context `{FinMap K M}.
@@ -11,3 +11,14 @@ Section map_disjoint.
     m2 !! i = None → m1 ##ₘ {[ i := x ]} ∪ m2 → m2 ##ₘ <[i:=x]> m1 ∧ m1 !! i = None.
   Proof. intros. solve_map_disjoint. Qed.
 End map_disjoint.
+
+Section map_dom.
+  Context `{FinMapDom K M D}.
+
+  Lemma set_solver_dom_subseteq {A} (i j : K) (x y : A) :
+    {[i; j]} ⊆ dom D (<[i:=x]> (<[j:=y]> (∅ : M A))).
+  Proof. set_solver. Qed.
+
+  Lemma set_solver_dom_disjoint {A} (X : D) : dom D (∅ : M A) ## X.
+  Proof. set_solver. Qed.
+End map_dom.