rewrite [getElem_swap]
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ (swap x i j)[↑j] = x[↑i]
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ (if ↑j = ↑j then x[↑i] else if ↑i = ↑j then x[↑j] else x[↑j]) = x[↑i]