New bureacracy/coherence

Hi all,

I was investigating the simulation of LK cut-reduction in SKS (from a 
semantic point of view)
and I came across the following pair of proofs (notation as in Lutz's 
recent paper on proof nets and SKS):

[(A, f ) , (B,C)]
-----------------m
( [A,B] , [f, C])
----------------- up-t
( [A,B] , C)
----------------- s , plus some \sigmas
[ A , (B , C)]


and

[(A, f ) , (B,C)]
------------------- up-aw /down-aw (doesn't matter which, (it's coherent))
[(A, t ) , (B,C)]
--------------------- up-f
[ A , (B , C)]

Has anyone considered this kind of thing before?  The reason behind 
considering the two
equal would be admissibilty of sequent calculus cut reduction in SKS 
(specifically
reduction of cut against contraction).  It also looks like the kind of 
coherence you might want to
hold of a categorical medial law.

Thanks,  Richard