proposition: Lemma noduplicates_Nth_same : forall l, (forall n1 n2 x, Nth n1 l x -> Nth n2 l x -> n1 = n2) -> noduplicates l.
proof: Proof. Proof using. introv NL. induction l; constructors. { introv I. lets (n&N): mem_Nth (rm I). forwards* Ab: NL Nth_zero Nth_succ. inverts Ab. } { apply IHl. introv N1 N2. forwards G: NL. applys Nth_succ N1. applys Nth_succ N2. inverts~ G. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)