proposition: Lemma permutation_in: forall l l' a, permutation eqA_dec l l' -> In a l -> exists a', eqA a' a /\ In a' l'.
proof: Proof. intros. destruct (multiplicity_in eqA eqA_dec l' a) as [a' [aa' a'l']]. rewrite <- (H a); trivial. apply in_multiplicity; trivial. exists a'; split; trivial. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)