
PROBABLY AT THE END OF dl.tex

Display calculi depend crucially on the \emph{display property},
which says that any substructure can be \emph{displayed}, that is, any
sequent is provably equivalent to some sequent in which the desired
substructure occupies the entire antecedent or succedent of the sequent.

The following lemma was not in fact required for any other proof;
however the steps taken in many other proofs reflected the fact that the
display property holds.

\begin{lemma}
Let $X$ be a substructure of $Y$, and let $\mathcal S$ be 
either $Z \vdash Y$ or $Y \vdash Z$.
Then there exists a sequent $\mathcal S'$ which has $X$ displayed 
(ie, for some $W$, $\mathcal S'$ is either $W \vdash X$ or $X \vdash W$),
and where $\mathcal S$ and $\mathcal S'$ are inter-derivable in \filldc.
\end{lemma}

\begin{verbatim}
fill_disp : "[| (?X, ?Y) : substr;
  ?seq = ($?Z |- $?Y) | ?seq = ($?Y |- $?Z); seq_LtGtOK ?seq |] ==>
  EX W. derrec (rulefs rlscfb) {$W |- $?X} = derrec (rulefs rlscfb) {?seq} |
    derrec (rulefs rlscfb) {$?X |- $W} = derrec (rulefs rlscfb) {?seq}"
\end{verbatim}

SOMEWHERE in eqdlshallow.tex

We also have that the shallow nested calculus obeys an analogue of the display
property. 

\begin{lemma}
Let $X$ be a sub-nested-sequent of $Y$, and let $\mathcal S$ be 
either $Z \seq Y$ or $Y \seq Z$.
Then there exists a sequent $\mathcal S'$ which has $X$ displayed 
(ie, for some $W$, $\mathcal S'$ is either $W \seq X$ or $X \seq W$),
and where $\mathcal S$ and $\mathcal S'$ are inter-derivable in \fillsn.
\end{lemma}

\begin{verbatim}
fill_n_disp : "[| (?X, ?Y) : subnseq;
  ?seq = ($?Z => $?Y) | ?seq = ($?Y => $?Z) |] ==> EX W.
  derrec (nrulefs snb_rlscf) {$W => $?X} = derrec (nrulefs snb_rlscf) {?seq} |
  derrec (nrulefs snb_rlscf) {$?X => $W} = derrec (nrulefs snb_rlscf) {?seq}"
\end{verbatim}


