diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 75aeb3099219c48cc051a045e4a857448c663052..4d9d66ef5e720994e4f89284e588d7bfd497db93 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -177,7 +177,7 @@ Qed.
 Lemma size_dom `{!Elements K D, !FinSet K D} {A} (m : M A) :
   size (dom D m) = size m.
 Proof.
-  rewrite dom_alt, list_to_set_size.
+  rewrite dom_alt, size_list_to_set.
   2:{ apply NoDup_fst_map_to_list. }
   unfold size, map_size. rewrite fmap_length. done.
 Qed.
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 0f81651da7423145efc9f79995a8273d4fb4385d..14aef32f7ea7dfdca45fd550e907103ad6d04699 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -203,7 +203,7 @@ Proof.
   by apply size_non_empty_iff, non_empty_difference.
 Qed.
 
-Lemma list_to_set_size l :
+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.