exact List.nodup_of_nodup_map nodup
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.Nodup l'
no goals