proposition: Lemma Permutation_eqlistA_commute l₁ l₂ l₃ : eqlistA eqA l₁ l₂ -> Permutation l₂ l₃ -> exists l₂', Permutation l₁ l₂' /\ eqlistA eqA l₂' l₃.
proof: Proof. intros E P. revert l₁ E. induction P; intros. - inversion_clear E. now exists nil. - inversion_clear E. destruct (IHP l0) as (l0',(P',E')); trivial. clear IHP. exists (x0::l0'). split; auto. - inversion_clear E. inversion_clear H0. exists (x1::x0::l1). now repeat constructor. - clear P1 P2. destruct (IHP1 _ E) as (l₁',(P₁,E₁)). destruct (IHP2 _ E₁) as (l₂',(P₂,E₂)). exists l₂'. split; trivial. econstructor; eauto. Qed.
imports: Permutation SetoidList