proposition: Lemma NoDup_Permutation_bis l l' : NoDup l -> length l' <= length l -> incl l l' -> Permutation l l'.
proof: Proof. intros. apply NoDup_Permutation; auto. - now apply NoDup_incl_NoDup with l. - split; auto. apply NoDup_length_incl; trivial. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat