Relation between `map_seq` and `set_seq`.

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.