proposition: Lemma dom_list_to_map {A} (l : list (K * A)) : dom (list_to_map l : M A) ≡ list_to_set l.*1.
proof: Proof. induction l as [|?? IH]. - by rewrite dom_empty. - simpl. by rewrite dom_insert, IH. Qed.
imports: stdpp(options)