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. now rewrite equivlistA_nil_eq by now symmetry. 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: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads