proposition: Lemma singleton_member a : a in {{a}}.
proof: Proof. unfold member. assert (a/{{a}} = 1); [idtac | lia]. apply singleton_mult_in; auto with sets. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)