grind_9856.lean:6:0-6:8: warning: declaration uses `sorry`