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