your memory of the path here is not what you'd generate by telling the story and observing the telling
because you can only see what seeable from where you are, and where you are was unseeable when you started
tell it again. you'll miss some stuff that's now unseeable from here, and you'll *add* some stuff that is *now* seeable from here
this *always* generates a second step, even if the second step is "do it again"
when you feel yourself spastically searching, *roving*, even: (1) resolve the specific shape of the logical obstruction. might have to be by negative geometry, adding up constraints that are keeping you from settling. then: (2) hold the shape in your hand, (3) rewind *to your own beginning* while keeping that shape in hand, and (4) walk the path again while holding the shape up to the skyline, looking for a match. theory: while you're holding that shape in your hand, *you won't be able to end up in the same search-space that you got stuck in*.
> So this theorem needs Q' to be an atom
I fucking love this kind of thing. aborting the search because upstream needs to do a better job of typing (as in tighting types)
> Ha! Yes - the typing is doing the work. The theorems were pretending they didn't need to know what Q' was, and the proof kept stalling because it DID need to know. Making hQ'_atom explicit in the signature isn't adding a requirement - it's admitting one that was always there.