proposition: Lemma permut_eqA : forall l l', Forall2 eqA l l' -> permutation _ eqA_dec l l'.
proof: Proof. induction 1. - apply permut_refl. - apply permut_cons_eq; trivial. Qed.
imports: Lia Relations Multiset SetoidList Permutation