case step.inr nki =>
  split
  case inl kj => simp [kj, Vec.get_swap_left]
  case inr nkj => rw [Vec.get_swap_neq _ i j k nki nkj]
n first last : Nat
α✝ : Type
arr1 arr2 arr✝ arr'✝ : Vec α✝ n
i j : Fin n
fi : first ≤ ↑i
ij : i ≤ j
jl : ↑j ≤ last
p : permuted n first last (arr✝.swap i j) arr'✝
ih : ∀ (k : Fin n), (arr✝.swap i j)[k] = arr'✝[p.to_map k]
k : Fin n
nki : ¬k = i
⊢ arr✝[k] = (arr✝.swap i j)[if k = j then i else k]
no goals