Theorem: SciLean.StructType.structMake_structProj (SciLean/Data/StructType/Basic.lean)

State before:
X : Sort u_1
I : Sort u_2
XI : I → Sort u_3
inst✝ : StructType X I XI
x : X
⊢ (structMake fun i => structProj x i) = x
Tactic:
apply right_inv
State after:
no goals