. apply Fin.ne_of_val_ne
  exact Nat.ne_of_gt (Nat.lt_of_le_of_lt jl gt)
case step.kj
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
k : Fin n
gt : last < ↑k
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
no goals