Re: A cut-free CoS system for S5

I agree with Greg. Displaying is a type of deep inference. But it is
not the same. Also, to my knowledge, nowhere in the display literature
is there any mention of the idea of rewriting at any depth. This is
explicit in CoS and in the rewriting literature of course. I would
even argue that there are reasons why we might want to avoid deep
inference. That is, it should be derivable but not necessarily built
in from the start to make sure that our rules capture substitution
properly. 

raj