I'm reading this paper by Kakutani :
http://nicosia.is.s.u-tokyo.ac.jp/~kakutani/files/aplas07.pdf
but I can't see how to use naturality of $m$ (given by the monoidal endofunctor modelling $\Box$) to prove categorical soundness of the calculus defined in Table 2 of that paper.
Does it involve the definition of $m^\ast$ given in order to interpret the Box-rule? If so, how does it work?