. apply Fin.ne_of_val_ne
  exact Nat.ne_of_lt (Nat.lt_of_lt_of_le lt fi)
case step.ki
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
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 : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ i

case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
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 : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j
case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
lt : ↑k < first
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 : arr'✝[k] = (arr✝.swap i j)[k]
⊢ k ≠ j