\newcommand{\mode}{\mbox{\textrm{mode}}}

\newcommand{\Tn}{\overline{T_n}}

Let $q\hastype A_1\KImp\dots\KImp A_n\KImp\prop$ and
$\mode(q)=m_1\mdots m_n$ be a \emph{mode} for $q$, where erach $m_i$
is eother $+$ (rigid) or $-$ (flex). An atom $q\ \Tn$ \emph{satisfies}
a mode $m_q=\mode(q)$ if for every $1\leq i\leq n$:
\beq
m_i= + & iff & T_i \mbox{ is rigid}\\
m_i= - & iff & T_i \mbox{ is flex}\\
\eneq
$\top_q$ satisfies $m_q$. $D_1\And D_2$ satisfies $m_q$ if so does
every $D_i$.

A signature $\Sigma$ is \emph{interesting} if every sort declared
therein contains at leat two distinct elements. A generalized variable
$E\ \Phi$ is \emph{constrained} if there is $x\in\Phi$ such that
$\Phi(x)\not= u$.


\begin{Lemma}
\label{le:moderigflex}
Let $\Sigma$ be intersesting and $M$ a $\Sigma$-term:
\ben
\item If $M$ is rigid, so is every $N\in\mnot(M)$.
\item If $M$ is a constrained generalized variable, so is every $N\in\mnot(M)$.
\enen
\end{Lemma}
\begin{proof}
By induction on the structure of $\mnot(M)$. For the first case, the
requirment for the signature to be intersting makes $\mnot(N)$ not
empty in the base case. Analogously for the requirment on variables.
\end{proof}

\begin{Lemma}
If $q\ \Tn$ satisfies $m_q$, so does $\mnotd(q\ \Tn)$.

\end{Lemma}
