proposition: Lemma IN_eqA_compat : forall ss x x', In x' ss -> x =A= x' -> In x ss.
proof: Proof. unfold eqA,Term.eqA; intros; subst; trivial. Qed.
imports: CoLoR(AccUtil MultisetOrder ListExtras RelExtras MultisetCore MultisetList MultisetTheory MultisetListOrder VTerm RelUtil LogicUtil) Coq(Permutation Arith Setoid)