iterate rewrite [swap_eq]
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ swap x i j = swap x j i
α : Type u
n : Nat
x : SizedArray α n
i j : Fin n
⊢ set (set x i x[↑j]) j x[↑i] = set (set x j x[↑i]) i x[↑j]