simpExtraArgsBug.lean:21:4-21:17: warning: declaration uses `sorry`