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