simp [permuted.to_map, fk, kl]
case refl
n first last : Nat
α✝ : Type
arr1 arr2 arr✝ : Vec α✝ n
k : Fin n
fk : first ≤ ↑k
kl : ↑k ≤ last
⊢ ∃ k', permuted.refl.to_map k' = k ∧ first ≤ ↑k' ∧ ↑k' ≤ last
no goals