proposition: Lemma map_img_kmap_L `{FinMap K M, FinMap K2 M2, SemiSet A SA, !LeibnizEquiv SA} (f : K → K2) `{!Inj (=) (=) f} m : map_img (kmap (M2:=M2) f m) =@{SA} map_img m.
proof: Proof. unfold_leibniz. by apply map_img_kmap. Qed.
imports: Coq(Permutation) stdpp(options)