proposition: Lemma NoDup_nth l d : NoDup l <-> (forall i j, i<length l -> j<length l -> nth i l d = nth j l d -> i = j).
proof: Proof. rewrite NoDup_nth_error. split. - intros H i j ? ? E. apply H; [assumption|]. now rewrite !(nth_error_nth' l d), E. - intros H i j ? E. assert (j < length l). { apply nth_error_Some. rewrite <- E. now apply nth_error_Some. } apply H; [assumption ..|]. rewrite !(nth_error_nth' l d) in E; congruence. Qed.
imports: PeanoNat