proposition: Lemma dom_finite {A} (m : M A) : set_finite (dom m).
proof: Proof. induction m using map_ind; rewrite ?dom_empty, ?dom_insert. - by apply empty_finite. - apply union_finite; [apply singleton_finite|done]. Qed.
imports: stdpp(options)