proposition: Lemma PermutationA_preserves_NoDupA l₁ l₂ : PermutationA l₁ l₂ -> NoDupA eqA l₁ -> NoDupA eqA l₂.
proof: Proof. induction 1; trivial. - inversion_clear 1; constructor; auto. apply PermutationA_equivlistA in H0. contradict H2. now rewrite H, H0. - inversion_clear 1. inversion_clear H1. constructor. + contradict H. inversion_clear H; trivial. elim H0. now constructor. + constructor; trivial. contradict H0. now apply InA_cons_tl. - eauto. Qed.
imports: Permutation SetoidList