fact: Definition kmap `{∀ A, Insert K2 A (M2 A), ∀ A, Empty (M2 A), ∀ A, MapFold K1 A (M1 A)} {A} (f : K1 → K2) (m : M1 A) : M2 A := list_to_map (fmap (prod_map f id) (map_to_list m)).
imports: Coq(Permutation) stdpp(options)