proposition: Lemma map_union : forall A B C (IB:Inhab B) (IC:Inhab C) (f:A->B->C) M1 M2, map_ f (M1 \u M2) = (map_ f M1) \u (map_ f M2).
proof: Proof. Proof using. intros. applys extensionality_of_dom_eq. { rewrite dom_union. repeat rewrite* dom_map. rewrite* dom_union. } { intros k Hk. rewrite* dom_map in Hk. lets Hk': Hk. rewrite* dom_union in Hk'. rew_set in Hk'. repeat rewrite* (@read_map A B C IB). repeat rewrite read_union_cases. rewrite* dom_map. case_if. { rewrite* (@read_map A B C IB). } { rewrite* (@read_map A B C IB). } } Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)