proposition: Lemma NoDupA_equivlistA_decompose l1 l2 : NoDupA eqA l1 -> NoDupA eqA l2 -> equivlistA eqA l1 l2 -> exists l, Permutation l1 l /\ eqlistA eqA l l2.
proof: Proof. intros. apply PermutationA_decompose. now apply NoDupA_equivlistA_PermutationA. Qed.
imports: Permutation SetoidList