grind_cutsat_upper_bug.lean:8:0-8:7: warning: declaration uses `sorry`