proposition: Lemma map_to_list_fmap {A B} (f : A → B) (m : M A) : map_to_list (f <$> m) ≡ₚ prod_map id f <$> map_to_list m.
proof: Proof. assert (NoDup ((prod_map id f <$> map_to_list m).*1)). { erewrite <-list_fmap_compose, (list_fmap_ext _ fst) by done. apply NoDup_fst_map_to_list. } rewrite <-(list_to_map_to_list m) at 1. by rewrite <-list_to_map_fmap, map_to_list_to_map. Qed.
imports: Coq(Permutation) stdpp(options)