simp [Vec.set, getElem]
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ (v.set i h₁ a)[j] = v[j]
α : Type
n i j : Nat
a : α
v : Vec α n
h₁ : i < n
h₂ : j < n
ne : i ≠ j
⊢ get ⟨v.val.set ⟨i, ⋯⟩ a, ⋯⟩ j h₂ = v.get j h₂