nestedtc.lean:30:9-30:21: warning: declaration uses `sorry`