% closed to open example with tensor eliminated
% to be called after resid.tex
\begin{Examplen}
\beq
cloz & : & closed\ z\\
clolam &: & \Pi E:exp.\ closed\ (lam\ E) \If \PI {x } {exp}\ (closed\ x) 
\Imp closed\ (E\ x)\\
cloapp &: & \Pi E_{1}E_{2}:exp.\ closed\ (app\ E_{1} E_{2}) \If 
closed\ E_1 \And closed\ E_{2}\\
\eneq
Let $def(closed)= \{cloz,clolam,cloapp\}$

\beq
\mnotd cloz & = &\mnotd closed\ z\\
            & = &\{\neg closed\ N\mid N\in\mnot z\}\\
            & = &\{ closed\ lam\ F, closed\ app\ F_{1} \ F_{2}\}\\
\vsk
\mnotd clolam & = &\mnotd (closed\ lam\ E) \cup
\neg closed\ (lam\ E) \If \mnotg (\PI {x } {exp}\ (closed\ x) \Imp closed\ 
(E\ x))\\
              & = &\{\neg closed\ N\mid N\in\mnot lam\ E\}\cup
\neg closed\ (lam\ E) \If \mnotg (\PI {x } {exp}\ (closed\ x) \Imp closed\ 
(E\ x))\\
              & = &\{closed\ z, closed\ app\ F_{1} \ F_{2},  
\neg closed\ (lam\ E) \If \PI {x } {exp}\ (closed\ x) \Imp \neg closed\ 
(E\ x))\\
\vsk
\mnotd cloapp & = & \mnotd closed\ (app\ E_{1} E_{2})\cup
\mnotg ( closed\ (app\ E_{1} E_{2}) \If closed\ E_1 \And closed\ 
E_{2})\}\\
              & = & {\neg closed\ N\mid N\in\mnot closed\ (app\ E_{1} 
E_{2})\}\cup\mnotg ( closed\ (app\ E_{1} E_{2}) \If closed\ E_1 \And 
closed\ E_{2})\\
              & = &\{closed\ z,  closed\ app\ F_{1} \ F_{2}, \neg closed\ (app\ E_{1} E_{2}) \If
\neg closed\ E_1 \Or \neg closed\ E_{2})
\eneq
Now, $def(\neg closed) = (\mnotd cloz) \otimes (\mnotd clolam) 
\otimes (\mnotd cloapp)$, \ie:
\beq
\Pi E : exp.\ \neg closed\ (lam\ E) \If \PI {x } {exp}\ closed\ x \Imp 
\neg closed\ (E\ x)\\
\Pi E_{1}E_{2}:exp.\ \neg closed\ (app\ E_{1} E_{2}) \If 
\neg closed\ E_1 \Or \neg closed\ E_{2}
\eneq
which by renaming and irrelevance of augmentation \ref{??} is 
equivalent to the expected definition of \texttt{open} on the same 
signature:
\beq
oplam &: & \Pi E : exp.\ open\ (lam\ E)  \If \PI {x } {exp}\ open\ (E\ x)\\
opapp &: & \Pi E_{1}E_{2}:exp.\ open\ (app\ E_{1} E_{2}) \If open\ E_1 \Or open\ E_{2}
\eneq
\end{Examplen}