proposition: Lemma map_id : forall A B (IB:Inhab B) (f:A->B->B) M, (forall x y, x \indom M -> y = M[x] -> f x y = y) -> map_ f M = M.
proof: Proof. Proof using. intros. applys extensionality_of_dom_eq. { rewrite* dom_map. } { intros k Hk. rewrite* dom_map in Hk. rewrite* (@read_map A B B IB). } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)