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
⊢ first ≤ ↑(permuted.refl.to_map k) ∧ ↑(permuted.refl.to_map k) ≤ last
no goals