proposition: Lemma NoDupA_equivlistA_PermutationA l₁ l₂ : NoDupA eqA l₁ -> NoDupA eqA l₂ -> equivlistA eqA l₁ l₂ -> PermutationA l₁ l₂.
proof: Proof. intros Pl₁. revert l₂. induction Pl₁ as [|x l₁ E1]. - intros l₂ _ H₂. symmetry in H₂. now rewrite (equivlistA_nil_eq eqA). - intros l₂ Pl₂ E2. destruct (@InA_split _ eqA l₂ x) as [l₂h [y [l₂t [E3 ?]]]]. { rewrite <-E2. intuition. } subst. transitivity (y :: l₁); [intuition |]. apply PermutationA_cons_app, IHPl₁. + now apply NoDupA_split with y. + apply equivlistA_NoDupA_split with x y; intuition. Qed.
imports: Permutation SetoidList