@dave: I don't have a reference; it seems to be just a consequence of soundness. By induction, the diagram corresponding to every term has the property that no "light" and "dark" sides are plugged together. @Peter: great, then I'll have another paper to cite! I agree that it is essentially a similar proof. The setting is slightly different, e.g. you don't identify the two duals of an object (the dual from the rigid structure and the light/dark dual). This actually simplifies the proof a bit. But yes, it's a very similar idea.