proposition: Lemma noduplicates_Nth_same_inv : forall l n1 n2 x, noduplicates l -> Nth n1 l x -> Nth n2 l x -> n1 = n2.
proof: Proof. Proof using. introv NL. gen n1 n2. induction NL; introv N1 N2. { inverts N1. } { inverts N1 as N1; inverts N2 as N2; autos~. { apply Nth_mem in N2. false*. } { apply Nth_mem in N1. false*. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)