proposition: Lemma dom_kmap `{!Elements K D, !FinSet K D, FinMapDom K2 M2 D2} {A} (f : K → K2) `{!Inj (=) (=) f} (m : M A) : dom (kmap (M2:=M2) f m) ≡@{D2} set_map f (dom m).
proof: Proof. apply set_equiv. intros i. rewrite !elem_of_dom, (lookup_kmap_is_Some _), elem_of_map. by setoid_rewrite elem_of_dom. Qed.
imports: stdpp(options)