proposition: Lemma for_multiset_empty_incl : forall A (E:multiset A), \{} \c E.
proof: Proof. Proof using. intros. apply empty_incl. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)