proposition: Lemma permutation_Permutation : forall l l', permutation _ eqA_dec l l' <-> exists l'', Permutation l l'' /\ Forall2 eqA l'' l'.
proof: Proof. split; intro H. - induction l in l', H |- *. + exists []; apply permut_sym, permut_nil in H as ->; auto using Forall2. + pose proof H as H'. apply permut_cons_InA, InA_split in H as (l1 & y & l2 & Heq & ->); trivial. apply permut_remove_hd_eq, IHl in H' as (l'' & IHP & IHA); clear IHl; trivial. apply Forall2_app_inv_r in IHA as (l1'' & l2'' & Hl1 & Hl2 & ->). exists (l1'' ++ a :: l2''); split. * apply Permutation_cons_app; trivial. * apply Forall2_app, Forall2_cons; trivial. - destruct H as (l'' & H & Heq). apply permut_trans with l''. + apply Permutation_impl_permutation; trivial. + apply permut_eqA; trivial. Qed.
imports: Lia Relations Multiset SetoidList Permutation