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.