proposition: Lemma Permutation_NoDup l l' : Permutation l l' -> NoDup l -> NoDup l'.
proof: Proof. induction 1; auto. - inversion_clear 1; constructor; eauto using Permutation_in. - inversion_clear 1 as [|? ? H1 H2]. inversion_clear H2; simpl in *. constructor. + simpl; intuition. + constructor; intuition. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat