intro h i j hxij
case mpr
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
⊢ (∀ (i j : Fin n), x[↑i] = x[↑j] → i = j) → ∀ (i j : Fin (Array.size x.val)), x.val[↑i] = x.val[↑j] → i = j
case mpr
α : Type u
n : Nat
inst✝ : DecidableEq α
x : SizedArray α n
h : ∀ (i j : Fin n), x[↑i] = x[↑j] → i = j
i j : Fin (Array.size x.val)
hxij : x.val[↑i] = x.val[↑j]
⊢ i = j