induction p with
| refl => rfl
| step i j fi ij jl p ih =>
  rw [ih]
  rw [Vec.get_swap_neq _ i j k]
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt (Nat.lt_of_le_of_lt (Nat.le_trans ij jl) gt)
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_gt (Nat.lt_of_le_of_lt jl gt)
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
p : permuted n first last arr1 arr2
k : Fin n
gt : last < ↑k
⊢ arr2[k] = arr1[k]
no goals