intro h
X : Sort u_2
I : Sort u_3
XI : I → Sort u_1
inst✝ : StructType X I XI
x x' : X
⊢ (∀ (i : I), structProj x i = structProj x' i) → x = 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
⊢ x = x'