proposition: Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) : dom (map_seq start (M:=M A) xs) ≡ set_seq start (length xs).
proof: Proof. revert start. induction xs as [|x xs IH]; intros start; simpl. - by rewrite dom_empty. - by rewrite dom_insert, IH. Qed.
imports: stdpp(options)