OK, replying to myself for future reference. I found the answer here: https://youtu.be/0GeJdTTzaDo (incidentally, that series of videos seems to have solutions for most of these problems).
The answer is that the left and right side of the notch holds local equivalents to the global "given X, prove Y" connectors. You can use the left side of the notch as an input, and you can connect that up through the global blocks to prove the hypothesis.
That was non-obvious! Also, the technique of connecting the output first and making connections to nothing to see what the implied proposition is was very useful - I should have thought of that.
The answer is that the left and right side of the notch holds local equivalents to the global "given X, prove Y" connectors. You can use the left side of the notch as an input, and you can connect that up through the global blocks to prove the hypothesis.
That was non-obvious! Also, the technique of connecting the output first and making connections to nothing to see what the implied proposition is was very useful - I should have thought of that.