exact Array.get_set_ne (j := j.val) a.val ⟨i, by simp [a.property, i.isLt]⟩ v
  (by simp [a.property, j.isLt]) (Fin.val_ne_of_ne h)
α : Type
n : Nat
a : Vec α n
i j : Fin n
v : α
h : i ≠ j
⊢ (a.val.set ⟨↑i, ⋯⟩ v)[↑j] = a.val[↑j]
no goals