dsimp [Nodup]
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ Nodup x ↔ ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ Array.Nodup x.val ↔ ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j