proposition: Lemma singleton_member_eqA a b : a in {{b}} -> a =A= b.
proof: Proof. intro h. destruct (eqA_dec a b); trivial. absurd (mult a {{b}} > 0); trivial. rewrite singleton_mult_notin; trivial. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)