proposition: Lemma member_pair x y z : x in {{y,z}} -> x =A= y \/ x =A= z.
proof: Proof. intro H. case (eqA_dec x y); [auto | intro x_neq_y]. case (eqA_dec x z); [auto | intro x_neq_z]. assert (x/{{y, z}} = 0). mset_unfold. rewrite union_mult. rewrite !singleton_mult_notin; trivial. unfold member in H. rewrite H0 in H; lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)