proposition: Lemma dom_union : forall A B (M N : map A B), dom (M \u N) = dom M \u dom N.
proof: Proof. Proof using. intros. simpl. unfold dom_impl, union_impl. rew_set. intros x. rew_set. iff R; destruct* (N x). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)