:: \DEEPCLOSE(G^c_n,S)
\rangle
\\[1ex]
- \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~
+ \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~ n\geq 1}
+ \\[1ex]
+ \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
\Gamma' = \ZEROPOS(G^o_n)
\land \tau' = \REMOVEGOALS(G^c_n,\tau)
\land \kappa' = \REMOVEGOALS(G^o_n,\kappa)