proposition: Lemma eq_proof : equivalence A eq_A.
proof: Proof. constructor; red. reflexivity. intros; transitivity y; assumption. intros; symmetry; assumption. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)