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

\INCLUDE{int.cam}
\INCLUDE{seq.cam}
$\begin{array}{l}
ffinv:A \pfunc{B} \tfunc{B \pfunc{{\set{A}}}} \\ ffinv(f) \deff \\ \rule{3ex}{0pt}  \left( \begin{array}{c}
 b \\ \{a \asor a \in 
dom(f) \wedge 
 f(a) = b\} 
\end{array} \right)_{b \in 
ran(f)}
\end{array}$

\traco

$\begin{array}{l}
ff2seq:B \times int \pfunc{B} \tfunc{{B^{\star}}} \\ ff2seq(b,f) \deff \\ \rule{3ex}{0pt}  
\LET 
l = 
seqInseg(
intMAX(
dom(f))) 
\IN \enlist{
\COND{
i \in 
dom(f)}{ f(i)}{b} \asor i \in l} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
ff2ffs:A \pfunc{B} \times C \times C \tfunc{{\set{C \pfunc{B}}}} \\ ff2ffs(f,na,nb) \deff \\ \rule{3ex}{0pt}  \{\left( \left(\!\! \begin{array}{c}
 na \\ a 
\end{array}\!\! \right) \left(\!\! \begin{array}{c}
 nb \\  f(a) 
\end{array}\!\! \right) \right) \asor a \in 
dom(f)\}
\end{array}$

\traco

$\begin{array}{l}
ff2STRff:A \pfunc{B} \tfunc{str \pfunc{str}} \\ ff2STRff(fk) \deff \\ \rule{3ex}{0pt}  
\LET 
f = 
\LAMBDA{x}
\COND{\is{str}(x)}{x}{
\COND{\is{int}(x)}{
itoa(x)}{
\COND{\is{SYM}(x)}{
symstr(x)}{\!\!\mattt{
\mbox{\texttt{"ff2STRfferror"}}}}}} 
\IN \left( \begin{array}{c}
 
f(k) \\ 
f( fk(k)) 
\end{array} \right)_{k \in 
dom(fk)} 
\TEL
\end{array}$

\traco

$\begin{array}{l}
ffByIndex:A \pfunc{B} \times {A^{\star}} \tfunc{{B^{\star}}} \\ ffByIndex(f,l) \deff \\ \rule{3ex}{0pt}  \enlist{ f(a) \asor a \in l \wedge 
a \in 
dom(f)}
\end{array}$

\traco

$\begin{array}{l}
ffByIndex1:A \pfunc{B} \times {A^{\star}} \times B \tfunc{{B^{\star}}} \\ ffByIndex1(f,l,d) \deff \\ \rule{3ex}{0pt}  \enlist{
\COND{
a \in 
dom(f)}{ f(a)}{d} \asor a \in l}
\end{array}$

\traco
\end{document}
