proposition: Lemma finite_union_eq : forall A B (M N : map A B), finite (M \u N) = (finite M /\ finite N).
proof: Proof. Proof using. intros. unfold finite. rewrite dom_union. apply finite_union_eq. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)