We give a formal derivation of \texttt{closed} from \texttt{open} for the signature with \texttt{lam, app}:
  \[
\begin{array}{l}
\forall E:  open\ (E) \Bimp \\
\quad\exists E_{1}E_{2}:  E \ebe  (app\  E_1 E_2)\And (open\  E_{1} \Or open\  E_{2}). 
\Or \mbox{}\\
\quad\exists F :  E \ebe (lam\ F) \And (\Pi x:  \neg open\  x \Imp open\  (F x))\\
 \qquad \lead_{cp}\\
 \quad 
 Not(\exists E_{1}E_{2}:   E \ebe  (app\  E_1 E_2)\And (open\  E_{1} \Or open\  E_{2}). 
  \Or\mbox{}\\
\quad \exists F:  E \ebe (lam\ F) \And (\Pi x:  \neg open\  x \Imp open\  (F x)))\\
\qquad \lead_{Not}\\
\quad 
\forall E_{1}E_{2}: E \nebe (app\  E_1 E_2) \Or (\neg open\  E_{1} 
\And \neg open\  E_{2}).  \And \mbox{}\\
\quad (\forall F :   E \nebe (lam\ F) \Or (\Pi x:  \neg open\  x \Imp\neg open\  (F x))\\
\qquad\lead_{lift}\\
\quad \forall E_{1}E_{2}:   E \nebe (app\  E_1 E_2) \Or \exists 
E_{1}E_{2}:   E \ebe  (app\  E_1 E_2) \And (\neg open\  E_{1} \And \neg open\  
E_{2}) \And \mbox{} \\
\quad\forall F :   E \nebe (lam\ F) \Or (\exists F:  E \ebe  (lam\ F)) \And (\Pi x:   
\neg open\  x \Imp\neg open\  (F x))\\
\qquad\lead_{dnf}^{*}(1,2)\\
\quad 
1.\, 
 \forall E_{1}E_{2}F: E \nebe (app\  E_1 E_2) \And E \nebe (lam\ F) \Or 
 \mbox{}\\
\quad\forall F:  E \nebe (lam\ F)\Or\exists E_{1}E_{2} E \ebe  (app\  
E_1 E_2) \And (\neg open\  E_{1} \And \neg open\  E_{2}) \\

\qquad\lead_{disunify(E \nebe (app\  E_1 E_2) \And  E  \nebe (lam\ F))}\\
\quad
\fbox{$\bot$} \Or \forall F: E \nebe (lam\ F)\Or\exists E_{1}E_{2}: E \ebe  (app\  
E_1 E_2) \And (\neg open\  E_{1} \And \neg open\  E_{2})\\
\qquad\lead_{UE2(F),prettyp}\\
 \begin{tt}
 \begin{tabular}{l}
% closed (app\  E_1 E_2) \If closed E_1 ; closed E_2.
% \begin{verbatim}
closed (app E1 E2) <- closed E1 <- closed E2.
%\end{verbatim}
 \end{tabular}
 \end{tt}
\mbox{}\\
\qquad\lead_{dnf}^{*}\\
\quad 2.\, 
 \forall E_{1}E_{2}F: E \nebe (app\  E_1 E_2) \And (E \nebe (app\  
E_1 E_2) \Or\exists E_{1}E_{2}: E \ebe  (app\  E_1 E_2) \And \mbox{}\\
\quad (\neg open\  E_{1} \And \neg open\  E_{2})
 \And (\exists F:  E \ebe  (lam\ F)) \And (\Pi x:  \neg open\  x \Imp\neg open\  (F x))\\
\qquad\lead_{UE2(E_{1}E_{2})}\\
\quad
 \forall E_{1}E_{2}F: E \nebe (app\  E_1 E_2) \And (E \nebe (app\  
E_1 E_2) \Or\exists E_{1}E_{2}: E \ebe  (app\  E_1 E_2) \And\mbox{}\\
\quad (\neg open\  
E_{1} \And \neg open\  E_{2}) \And (\exists F:  E \ebe  (lam\ F)) \And (\Pi x:   
\neg open\  x \Imp\neg open\  (F x))\footnote{to be fixed}\\
\qquad\lead_{disunify(E \nebe (app\  E_1 E_2))} \\
\quad 
\exists F: E \ebe  lam\ F \And (\Pi x:   \neg open\  x \Imp\neg open\  (F 
x))\\
\qquad\lead_{prettyp}\\
 \begin{tt}
 \begin{tabular}{l}
% closed (lam E) \If ({x:exp} closed x \Imp closed (E x)).
%\begin{verbatim}
closed (lam E) <- ({x:exp} closed x <- closed (E x)).
%\end{verbatim}
  \end{tabular}
  \end{tt}
\end{array}
\]
