simp [Vec.set]
case a
α : Type
n i : Nat
a b : α
v : Vec α n
h : i < n
⊢ ((v.set i h a).set i h b).val = (v.set i h b).val
case a
α : Type
n i : Nat
a b : α
v : Vec α n
h : i < n
⊢ (v.val.set ⟨i, ⋯⟩ a).set ⟨i, ⋯⟩ b = v.val.set ⟨i, ⋯⟩ b