proposition: Lemma noduplicates_one : forall (x:A), noduplicates (x::nil).
proof: Proof. Proof using. intros. applys noduplicates_cons. { intros M. false* mem_nil_inv. } applys noduplicates_nil. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)