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_lt (Nat.lt_of_lt_of_le lt fi)
  . apply Fin.ne_of_val_ne
    exact Nat.ne_of_lt (Nat.lt_of_lt_of_le lt (Nat.le_trans fi ij))
n first last : Nat
α✝ : Type
arr1 arr2 : Vec α✝ n
p : permuted n first last arr1 arr2
k : Fin n
lt : ↑k < first
⊢ arr2[k] = arr1[k]
no goals