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