Some notes for the benefit of future-me:
The current situation is still feeling that the hard gap is between the multiple-conclusion and single-conclusion version of the calculus, which in a way puts me right back in spring semester 2004 when Frank first posed the problem; if there's some way of phrasing the soundness proof in terms of "normalizing away" all the letccs, though, that seems to have a much better chance of scaling up to the bunched setting than either my or noam's current proof.
