simp [Vec.get, Vec.set]
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ (a.set i v).get j = a.get j
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ (a.val.set ⟨↑i, ⋯⟩ v)[↑j] = a.val[↑j]