proposition: Lemma noduplicates_prefix: forall xs ys, noduplicates ys -> prefix xs ys -> noduplicates xs.
proof: Proof. Proof using. introv ? (zs&?). subst. forwards: noduplicates_app_inv; eauto. tauto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation LibList)