proposition: Lemma in_empty_inv : forall x, x \in (\{}:multiset A) -> False.
proof: Proof. Proof using. introv. apply notin_empty. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibList LibInt LibNat LibOperation LibEpsilon LibSet LibMonoid)