proposition: Lemma eqA_refl : forall x, x =A= x.
proof: Proof. rewrite eqA_eq; trivial. Qed.
imports: Coq(Transitive_Closure Compare_dec Relations Permutation Setoid Morphisms Basics Lia) CoLoR(RelExtras MultisetTheory ListPermutation MultisetCore ListExtras AccUtil LogicUtil)