proposition: Lemma Permutation_impl_permutation : forall l l', Permutation l l' -> permutation _ eqA_dec l l'.
proof: Proof. induction 1. - apply permut_refl. - apply permut_cons; auto using Equivalence_Reflexive. - change (x :: y :: l) with ([x] ++ y :: l); apply permut_add_cons_inside; simpl; apply permut_cons_eq; auto using Equivalence_Reflexive, permut_refl. - apply permut_trans with l'; trivial. Qed.
imports: Lia Relations Multiset SetoidList Permutation