rcases i with ⟨i,hi⟩
α : Type u
x : Subarray α
i j : Fin (size x)
⊢ (swap x i j)[↑i] = x[↑j]
case mk
α : Type u
x : Subarray α
j : Fin (size x)
i : Nat
hi : i < size x
⊢ (swap x { val := i, isLt := hi } j)[↑{ val := i, isLt := hi }] = x[↑j]