```
Require Import List.
Theorem aux n L (H: forall x, x < n -> In x L) (H0: length L = n): NoDup L.
```

It feels harder than the previous one (How to approach this (seemingly) simple theorem?). Or maybe I lack creativity/cleverness to imagine correct intermediate lemmas.

Can someone give hints? I tried doing induction on n, but I’m missing something.