subset.lean:33:0-33:7: warning: declaration uses `sorry`
subset.lean:37:0-37:7: warning: declaration uses `sorry`