Now I just need to understand how this all works out in the linear case so I can <ahahaha>magically and instantaneously solve all the problems of a more fully linear logical framework motivated by such a cut-elimination proof that have been open research problems essentially since Frank's 1994 tech report and assaulted vigorously since then by him and Iliano</ahahaha>. I will shake my fists spitefully at everyone I have failed to convince that deep down, despite all of my attempts at humility and accurate evaluation of my own intellectual abilities, I am really an arrogant bastard at heart.
Also had a bit of a double-piano jam session with Ann Lewis. It was pretty fun. I continue to be saddened by how many people aren't familiar with "While my guitar gently weeps", but now N has been reduced to N-1.