proposition: Lemma NoDup_permut : forall l l', NoDup l -> NoDup l' -> (forall x, In x l <-> In x l') -> permutation l l'.
proof: Proof. intros. red; unfold meq; intros. rewrite multiplicity_NoDup in H, H0. generalize (H a) (H0 a) (H1 a); clear H H0 H1. do 2 rewrite multiplicity_In. intros H H' [H0 H0']. destruct (multiplicity (list_contents l) a) as [|[|n]], (multiplicity (list_contents l') a) as [|[|n']]; [ tauto | | | | tauto | | | | ]; try solve [intuition auto with arith]; exfalso. - now inversion H'. - now inversion H. - now inversion H. Qed.
imports: Relations Setoid SetoidList List Multiset PermutSetoid Permutation