diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index 114ae30d4fd760ea54f39d939ff14cb99706f4f6..d020c1941639122aa4f2614156325a9ec1e059a0 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -143,3 +143,14 @@ Proof. unfold_leibniz; apply dom_difference. Qed.
 Lemma dom_fmap_L {A B} (f : A → B) (m : M A) : dom D (f <$> m) = dom D m.
 Proof. unfold_leibniz; apply dom_fmap. Qed.
 End fin_map_dom.
+
+Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
+  dom D (map_seq start xs) ≡ set_seq start (length xs).
+Proof.
+  revert start. induction xs as [|x xs IH]; intros start; simpl.
+  - by rewrite dom_empty.
+  - by rewrite dom_insert, IH.
+Qed.
+Lemma dom_seq_L `{FinMapDom nat M D, !LeibnizEquiv D} {A} start (xs : list A) :
+  dom D (map_seq start xs) = set_seq start (length xs).
+Proof. unfold_leibniz. apply dom_seq. Qed.