proposition: Lemma insert_meq M N a : insert a M =mul= insert a N -> M =mul= N.
proof: Proof. intros; apply multeq_meq; intro. set (w := (meq_multeq H) x). unfold insert in w. rewrite !union_mult in w. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(RelExtras MultisetCore ListPermutation NatUtil ListExtras LogicUtil)