proposition: Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' -> (forall x:A, In x l <-> In x l') -> Permutation l l'.
proof: Proof. intros N. revert l'. induction N as [|a l Hal Hl IH]. - destruct l'; simpl; auto. intros Hl' H. exfalso. rewrite (H a); auto. - intros l' Hl' H. assert (Ha : In a l') by (apply H; simpl; auto). destruct (Add_inv _ _ Ha) as (l'' & AD). rewrite <- (Permutation_Add AD). apply perm_skip. apply IH; clear IH. * now apply (NoDup_Add AD). * split. + apply incl_Add_inv with a l'; trivial. intro. apply H. + intro Hx. assert (Hx' : In x (a::l)). { apply H. rewrite (Add_in AD). now right. } destruct Hx'; simpl; trivial. subst. rewrite (NoDup_Add AD) in Hl'. tauto. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat