etaStruct.lean:49:4-49:19: warning: declaration uses `sorry`