hole in `(by _)` should be accepted locally

the proof should continue.