proposition: Lemma PermutationA_decompose l₁ l₂ : PermutationA l₁ l₂ -> exists l, Permutation l₁ l /\ eqlistA eqA l l₂.
proof: Proof. induction 1. - now exists nil. - destruct IHPermutationA as (l,(P,E)). exists (x₁::l); auto. - exists (x::y::l). split. + constructor. + reflexivity. - destruct IHPermutationA1 as (l₁',(P,E)). destruct IHPermutationA2 as (l₂',(P',E')). destruct (@Permutation_eqlistA_commute l₁' l₂ l₂') as (l₁'',(P'',E'')); trivial. exists l₁''. split. + now transitivity l₁'. + now transitivity l₂'. Qed.
imports: Permutation SetoidList