Re: Decomposition for classical logic

> It should be mentioned here (because it is nowhere published) that we 
> actually KNOW that this is true, i.e., it should be stated as theorem. 

Ah, right. I should have tried to symmetrise the fact that you can push 
down contraction inside a sequent calculus derivation once you allow it 
to apply deeply. I just checked, it works. So you proved the conjecture 
in my thesis!

> The nice thing about all these proof transformations is that they get well 
> along with my proof nets. This means that they do not change the underlying 
> net of the derivation.

What does that mean? Cut elimination should change the net, shouldn't it?

-Kai