diff --git a/prelude/collections.v b/prelude/collections.v
index 2b54cd0ca8d26005ae7eee19ba88f4263be75e8d..b34b5cdc32165f44049f1b0eb4b7fb0c510a129c 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -591,6 +591,11 @@ Definition set_finite `{ElemOf A B} (X : B) := ∃ l : list A, ∀ x, x ∈ X 
 
 Section finite.
   Context `{SimpleCollection A B}.
+  Global Instance set_finite_subseteq :
+     Proper (flip (⊆) ==> impl) (@set_finite A B _).
+  Proof. intros X Y HX [l Hl]; exists l; solve_elem_of. Qed.
+  Global Instance set_finite_proper : Proper ((≡) ==> iff) (@set_finite A B _).
+  Proof. by intros X Y [??]; split; apply set_finite_subseteq. Qed.
   Lemma empty_finite : set_finite ∅.
   Proof. by exists []; intros ?; rewrite elem_of_empty. Qed.
   Lemma singleton_finite (x : A) : set_finite {[ x ]}.
@@ -614,4 +619,10 @@ Section more_finite.
   Proof. intros [l ?]; exists l; intros x [??]%elem_of_intersection; auto. Qed.
   Lemma difference_finite X Y : set_finite X → set_finite (X ∖ Y).
   Proof. intros [l ?]; exists l; intros x [??]%elem_of_difference; auto. Qed.
+  Lemma difference_finite_inv X Y `{∀ x, Decision (x ∈ Y)} :
+    set_finite Y → set_finite (X ∖ Y) → set_finite X.
+  Proof.
+    intros [l ?] [k ?]; exists (l ++ k).
+    intros x ?; destruct (decide (x ∈ Y)); rewrite elem_of_app; solve_elem_of.
+  Qed.
 End more_finite.
diff --git a/prelude/fin_map_dom.v b/prelude/fin_map_dom.v
index e8169bf034f25fe67e6b10ee24899b4d578bbb52..7c4e76974aeb81104a670882203b2ecaef846b60 100644
--- a/prelude/fin_map_dom.v
+++ b/prelude/fin_map_dom.v
@@ -108,6 +108,11 @@ Proof.
   rewrite !elem_of_dom, lookup_fmap, <-!not_eq_None_Some.
   destruct (m !! i); naive_solver.
 Qed.
+Lemma dom_finite {A} (m : M A) : set_finite (dom D m).
+Proof.
+  induction m using map_ind; rewrite ?dom_empty, ?dom_insert;
+    eauto using empty_finite, union_finite, singleton_finite.
+Qed.
 
 Context `{!LeibnizEquiv D}.
 Lemma dom_empty_L {A} : dom D (@empty (M A) _) = ∅.