The mix rule
Arnaud Fleury, Christian Retoré · Mathematical Structures in Computer Science · 1994
We have found both a proofnet criterion and a sequent calculus for the multiplicative fragment with units ( ⊗1,℘,0, atoms), but without the ┴-boxes of Girard (1987), which differentiate between 1 and ┴. We have also proved that for any of our proofnets there is a corresponding sequential proof.