simp only [nodup_empty, true_iff]
case empty
α : Type u
inst✝ : DecidableEq α
⊢ Nodup #[] ↔ ∀ (i j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j
case empty
α : Type u
inst✝ : DecidableEq α
⊢ ∀ (i j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j