proposition: Lemma dom_kmap_L `{!Elements K D, !FinSet K D, FinMapDom K2 M2 D2} `{!LeibnizEquiv D2} {A} (f : K → K2) `{!Inj (=) (=) f} (m : M A) : dom (kmap (M2:=M2) f m) = set_map f (dom m).
proof: Proof. unfold_leibniz. by apply dom_kmap. Qed.
imports: stdpp(options)