proposition: Lemma PermutationA_equivlistA l₁ l₂ : PermutationA l₁ l₂ -> equivlistA eqA l₁ l₂.
proof: Proof. induction 1. - reflexivity. - now apply equivlistA_cons_proper. - now apply equivlistA_permute_heads. - etransitivity; eassumption. Qed.
imports: Permutation SetoidList