\documentclass{article}
\input camila.mac
\begin{document}

$\begin{array}{l}
monff:A \pfunc{B} \times A \pfunc{B} \times B \times B \pfunc{B} \tfunc{A \pfunc{B}} \\ monff(m,n,f) \deff \\ \rule{3ex}{0pt}  m \plus n \plus \left( \begin{array}{c}
 a \\ 
f( m(a), n(a)) 
\end{array} \right)_{a \in 
dom(m) \cap 
dom(n)}
\end{array}$

\traco

$\begin{array}{l}
monseq:{B^{\star}} \times {B^{\star}} \times B \times B \pfunc{B} \tfunc{{B^{\star}}} \\ monseq(l,r,f) \deff \\ \rule{3ex}{0pt}  
\COND{
l = \emptylist}{\emptylist}{
\COND{
r = \emptylist}{l}{\enlist{
f(
head(l),
head(r))} \conc 
monseq(
tail(l),
tail(r),f)}}
\end{array}$

\traco
\end{document}
