rw[← structMake_structProj (I:=I) x']
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ (structMake fun i => structProj x i) = x'
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
h : ∀ (i : I), structProj x i = structProj x' i
⊢ (structMake fun i => structProj x i) = structMake fun i => structProj x' i