proposition: Lemma list_to_map_to_list {A} (m : M A) : list_to_map (map_to_list m) = m.
proof: Proof. apply map_eq. intros i. apply option_eq. intros x. by rewrite <-elem_of_list_to_map, elem_of_map_to_list by auto using NoDup_fst_map_to_list. Qed.
imports: Coq(Permutation) stdpp(options)