proposition: Lemma union_empty_inv_multiset : forall A (l1 l2:multiset A), l1 \u l2 = \{} -> l1 = \{} /\ l2 = \{}.
proof: Proof. Proof using. intros. eapply union_empty_inv_inst. eauto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)