proposition: Lemma eq_proof : equivalence A eq_A.
proof: Proof. unfold eq_A; split. intro n; apply eq_refl. intros a1 a2 a3 H1 H2; rewrite H1; assumption. intros a1 a2 H; rewrite H; apply eq_refl. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)