proposition: Lemma permut_InA_InA : forall l1 l2 e, permutation l1 l2 -> InA eqA e l1 -> InA eqA e l2.
proof: Proof. intros l1 l2 e. do 2 rewrite multiplicity_InA. unfold permutation, meq. intros H;rewrite H; auto. Qed.
imports: Lia Relations Multiset SetoidList