Explicit programming style

We can program a solution to $\forall x\!:\!A.\ \exists y\!:\!B.\ S[x, y]$ directly by writing a function $f \in A \rightarrow B$ and then proving $\forall x\!:\!A.\ S[x, f(x)]$. Christine Paulin [94] is studying how to use the program information to help drive the derivation of the proof.