grind_eta_struct_internalize.lean:32:8-32:22: warning: declaration uses `sorry`