simpDischargeLoop.lean:42:8-42:21: warning: declaration uses `sorry`