proposition: Lemma member_singleton x y : x in {{y}} -> x =A= y.
proof: Proof. mset_unfold; intros. case (eqA_dec x y); [trivial | intro x_neq_y]. assert (x/{{y}} = 0); [auto with multisets | idtac]. rewrite H0 in H; lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)