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