proposition: Lemma list_to_map_fmap {A B} (f : A → B) l : list_to_map (prod_map id f <$> l) = f <$> (list_to_map l : M A).
proof: Proof. induction l as [|[i x] l IH]; csimpl; rewrite ?fmap_empty; auto. rewrite <-list_to_map_cons; simpl. by rewrite IH, <-fmap_insert. Qed.
imports: Coq(Permutation) stdpp(options)