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