question on formalism B

Hi Frogs,

I have a question, addressed in particular to those working on
"Formalism B", which is still somehow a mystery to me. I have some good 
understanding of what should be identified, but not of what SHOULD NOT be 
identified.

Can someone give me a simple example of two derivations that are not 
identified by "Formalism B", but are identified by proof nets (the 
N-nets of our TLCA-paper) ?

I guess that

    ([A,B],[C,D])
s ---------------
    [A,(B,[C,D])]
s ---------------
    [A,[(B,C),D]]

vs.

    ([A,B],[C,D])
s ---------------
    [([A,B],C),D]
s ---------------
    [[A,(B,C)],D]
= ---------------
    [A,[(B,C),D]]

should be the typical example. The two derivations above are identified by 
proof nets. But not by B, are they? Am I right or wrong about this?

In any case, an answer would also help clarifying the relation to 
categorical coherence.

Maybe we should introduce a third type of bureaucracy: Type C.
"Formalism C" then identifies the two derivations above.
The theorem would be

     "Formalism C"  =  proof nets  =  cat. coherence

Does this make sense?

-Lutz