proposition: Lemma NoDupA_equivlistA_permut : forall l l', NoDupA eqA l -> NoDupA eqA l' -> equivlistA eqA l l' -> permutation l l'.
proof: Proof. intros. red; unfold meq; intros. rewrite multiplicity_NoDupA in H, H0. generalize (H a) (H0 a) (H1 a); clear H H0 H1. do 2 rewrite multiplicity_InA. destruct 3; lia. Qed.
imports: Lia Relations Multiset SetoidList