proposition: Lemma map_img_fmap `{FinMap K M, FinSet A SA, SemiSet B SB} (f : A → B) (m : M A) : map_img (f <$> m) ≡@{SB} set_map (C:=SA) f (map_img m).
proof: Proof. apply set_equiv. intros y. rewrite elem_of_map_img, elem_of_map. setoid_rewrite lookup_fmap. setoid_rewrite fmap_Some. setoid_rewrite elem_of_map_img. naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)