proposition: Lemma r_eqA : Proper (eqA ==> eqA ==> impl) r.
proof: Proof. intros a b ab c d cd ac. eapply r_eqA_compat. apply ab. apply cd. hyp. Qed.
imports: Coq(List Permutation Arith Morphisms Basics) CoLoR(MultisetOrder RelExtras MultisetCore MultisetList MultisetTheory AccUtil RelUtil LogicUtil) CoLoR(AccUtil ListUtil)