apply congr_fun
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
f : (i : I) → XI i
i : I
⊢ structProj (structMake f) i = f i
case h
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
f : (i : I) → XI i
i : I
⊢ structProj (structMake f) = fun i => f i