proposition: Lemma map_img_fmap_L `{FinMap K M, FinSet A SA, SemiSet B SB, !LeibnizEquiv SB} (f : A → B) (m : M A) : map_img (f <$> m) =@{SB} set_map (C:=SA) f (map_img m).
proof: Proof. unfold_leibniz. apply map_img_fmap. Qed.
imports: Coq(Permutation) stdpp(options)