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

State before:
X✝ : Sort ?u.24013
I : Sort ?u.24012
XI : I → Sort ?u.24011
inst✝¹ : StructType X✝ I XI
X : Type u_1
inst✝ : Zero X
x : X
⊢ oneHot () x = x
Tactic:
rfl
State after:
no goals