diff --git a/CHANGELOG.md b/CHANGELOG.md
index 601a57ecb94c3fe2fa7eee3b007793a4efb2be93..6711265abc8cc3a2dbbfee377eb0d4f2f766efb0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -152,7 +152,7 @@ API-breaking change is listed.
   `map_filter_singleton_False`, `map_filter_comm`, `map_union_least`,
   `map_subseteq_difference_l`, `insert_difference`, `insert_difference'`,
   `difference_insert`, `difference_insert_subseteq`. (by Hai Dang)
-- Add `map_size_disj_union`.
+- Add `map_size_disj_union`, `size_dom`, `size_list_to_set`.
 - Tweak reduction on `gset`, so that `cbn` matches the behavior by `simpl` and
   does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems)
 - Add `get_head` tactic to determine the syntactic head of a function
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index c9951d4a8d715cbc4410885cea2693983a24084a..4d9d66ef5e720994e4f89284e588d7bfd497db93 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -165,6 +165,23 @@ Proof.
   - simpl. by rewrite dom_insert, IH.
 Qed.
 
+(** Alternative definition of [dom] in terms of [map_to_list]. *)
+Lemma dom_alt {A} (m : M A) :
+  dom D m ≡ list_to_set (map_to_list m).*1.
+Proof.
+  rewrite <-(list_to_map_to_list m) at 1.
+  rewrite dom_list_to_map.
+  done.
+Qed.
+
+Lemma size_dom `{!Elements K D, !FinSet K D} {A} (m : M A) :
+  size (dom D m) = size m.
+Proof.
+  rewrite dom_alt, size_list_to_set.
+  2:{ apply NoDup_fst_map_to_list. }
+  unfold size, map_size. rewrite fmap_length. done.
+Qed.
+
 Lemma dom_singleton_inv {A} (m : M A) i :
   dom D m ≡ {[i]} → ∃ x, m = {[i := x]}.
 Proof.
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 5f5168a7040b0f573c8a708fbf84f52cb1cb1094..14aef32f7ea7dfdca45fd550e907103ad6d04699 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -119,6 +119,15 @@ Proof. intros ?. rewrite elem_of_list_to_set. apply elem_of_elements. Qed.
 Lemma list_to_set_elements_L `{!LeibnizEquiv C} X : list_to_set (elements X) = X.
 Proof. unfold_leibniz. apply list_to_set_elements. Qed.
 
+Lemma elements_list_to_set l :
+  NoDup l → elements (list_to_set (C:=C) l) ≡ₚ l.
+Proof.
+  intros Hl. induction Hl.
+  { rewrite list_to_set_nil. rewrite elements_empty. done. }
+  rewrite list_to_set_cons, elements_disj_union by set_solver.
+  rewrite elements_singleton. apply Permutation_skip. done.
+Qed.
+
 (** * The [size] operation *)
 Global Instance set_size_proper: Proper ((≡) ==> (=)) (@size C _).
 Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
@@ -194,6 +203,13 @@ Proof.
   by apply size_non_empty_iff, non_empty_difference.
 Qed.
 
+Lemma size_list_to_set l :
+  NoDup l → size (list_to_set (C:=C) l) = length l.
+Proof.
+  intros Hl. unfold size, set_size. simpl.
+  rewrite elements_list_to_set; done.
+Qed.
+
 (** * Induction principles *)
 Lemma set_wf : wf (⊂@{C}).
 Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.