apply Subtype.eq
α : Type
n i : Nat
a b : α
v : Vec α n
h : i < n
⊢ (v.set i h a).set i h b = v.set i h b
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