cases hij
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
j : Nat
hj : j < n
hij : ↑i = j
⊢ (set x i v)[j] = if ↑i = j then v else x[j]
case refl
α : Type u
n : Nat
x : SizedArray α n
i : Fin n
v : α
hj : ↑i < n
⊢ (set x i v)[↑i] = if ↑i = ↑i then v else x[↑i]