proposition: Lemma empty_empty : forall M, (forall x, x / M = 0) -> M = empty.
proof: Proof. intros M mulM; destruct M. trivial. absurd (a / (a::M) = 0). simpl. destruct (eqA_dec a a); auto with sets. auto. Qed.
imports: Coq(Permutation PermutSetoid Lia Multiset) CoLoR(LogicUtil RelExtras MultisetCore ListExtras)