proposition: Lemma meq_ins_ins_eq a a' M M' : M + {{a}} =mul= M' + {{a'}} -> a =A= a' -> M =mul= M'.
proof: Proof. intros. cut (M + {{a}} =mul= M' + {{a'}}). rewrite H0; intro; apply meq_union_meq with {{a'}}; trivial. trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)