proposition: Lemma map_img_kmap `{FinMap K M, FinMap K2 M2, SemiSet A SA} (f : K → K2) `{!Inj (=) (=) f} m : map_img (kmap (M2:=M2) f m) ≡@{SA} map_img m.
proof: Proof. apply set_equiv. intros x. rewrite !elem_of_map_img. setoid_rewrite (lookup_kmap_Some f). naive_solver. Qed.
imports: Coq(Permutation) stdpp(options)