proposition: Lemma notin_empty : forall x, x \notin (\{}:multiset A).
proof: Proof. Proof using. intros. unfold notin. rewrite in_empty_eq. auto. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)