proposition: Lemma map_single : forall A B C (IB:Inhab B) (IC:Inhab C) (f:A->B->C) x y, map_ f (x \:= y) = (x \:= f x y).
proof: Proof. Proof using. intros. applys extensionality_of_dom_eq. { rewrite dom_single. repeat rewrite* dom_map. rewrite* dom_single. } { intros k Hk. rewrite* dom_map in Hk. lets Hk': Hk. rewrite* dom_single in Hk'. rew_set in Hk'. subst x. repeat rewrite* (@read_map A B C IB). do 2 rewrite read_single. auto. } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)