proposition: Lemma finite_union : forall A B (M N : map A B), finite M -> finite N -> finite (M \u N).
proof: Proof. Proof using. intros. rewrite* finite_union_eq. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)