diff --git a/doc/phd-project-2009-07/challenges.tex b/doc/phd-project-2009-07/challenges.tex
index 712e5b82c46804ff49de38993601c4a877383267..bfbcf8989e4cf036261be2e378d8f4235716d654 100644
--- a/doc/phd-project-2009-07/challenges.tex
+++ b/doc/phd-project-2009-07/challenges.tex
@@ -1,2 +1,45 @@
 \section{Reasoning}
+This section presents an example of proof of a specification. It should be
+noted that it does \emph{not} describe a general decision procedure for
+deciding the validity of such contracts. The mechanisms used are induction on
+data types (in this example, the primitive type of linked lists), and
+fold/unfold operations, that is inlining function calls and replacing
+expressions by equivalent function calls.
 
+We want to prove the third contract of Figure~\ref{fig:listset}:
+\begin{lstlisting}
+$\forall$ xs: List[Int], ys: List[Int], z: Int .
+  content(xs) = content(ys) $\rightarrow$ content(insert(z, xs)) = content(insert(z, ys))
+\end{lstlisting}
+
+We do it by induction on \K{xs}. For \K{xs = Nil}:
+\begin{lstlisting}
+content(Nil) = content(ys) $\rightarrow$ content(insert(z, Nil)) = content(insert(z, ys))
+\end{lstlisting} 
+By unfolding \K{content(Nil)} and \K{insert(z, Nil)} we get:
+\begin{lstlisting}
+Set.empty = content(ys) $\rightarrow$ content(z :: Nil) = content(insert(z, ys))
+\end{lstlisting}
+By folding \K{content(ys)}, we get that for the left hand side to be true, we need \K{ys} to be \K{Nil}. We thus have:
+\begin{lstlisting}
+Set.empty = Set.empty $\rightarrow$ content(z :: Nil) = content(insert(z, Nil))
+\end{lstlisting}
+\ldots and by unfolding \K{insert} and \K{content} we get to the correct statement:
+\begin{lstlisting}
+Set.empty = Set.empty $\rightarrow$ Set(z) = Set(z)
+\end{lstlisting}
+
+Now for the case where \K{x = x' :: xs'}, \K{y = y' :: ys'}, assuming
+that the statement holds for \K{xs'} and \K{ys'}:
+\begin{lstlisting}
+content(x' :: xs') = content(y' :: ys') $\rightarrow$ content(insert(z, x' :: xs')) = content(insert(z, y' :: ys'))
+\end{lstlisting}
+We unfold \K{content} and \K{insert}:
+\begin{lstlisting}
+content(xs') + x = content(ys') + y $\rightarrow$ content(z :: x' :: xs')) = content(z :: y' :: ys'))
+\end{lstlisting}
+We unfold \K{content} again:
+\begin{lstlisting}
+content(xs') + x = content(ys') + y $\rightarrow$ content(xs') + x' + z = content(ys') + y' + z
+\end{lstlisting}
+\ldots and the statement is clearly true.
diff --git a/doc/phd-project-2009-07/code/ListSet.scala b/doc/phd-project-2009-07/code/ListSet.scala
index d614bca2f4a8aefa689c662ad6d33ad95eb0305d..fb2c51373768ec005ee5b5e25bf9931066097e03 100644
--- a/doc/phd-project-2009-07/code/ListSet.scala
+++ b/doc/phd-project-2009-07/code/ListSet.scala
@@ -19,7 +19,7 @@ object ListSet {
     case x :: xs => content(xs) + x
   }
 
-  def insert(x: Int, xs: List[Int]): List[Int] = if(member(x, xs)) xs else insert(x, xs)
+  def insert(x: Int, xs: List[Int]): List[Int] = x :: xs
 
   def remove(x: Int, xs: List[Int]): List[Int] = xs match {
     case Nil => Nil
diff --git a/doc/phd-project-2009-07/future.tex b/doc/phd-project-2009-07/future.tex
index 02b12c8dde3e0cfc7a3c82c1df94760c0de41db9..fe823f4545bdd92e1b53434a1e8aa4519572c188 100644
--- a/doc/phd-project-2009-07/future.tex
+++ b/doc/phd-project-2009-07/future.tex
@@ -6,7 +6,7 @@ of {\tt scalac}, other more theoretical, such as how to automate fold/unfold
 reasoning techniques.
 
 \paragraph{Extension of {\purescala}}
-We would like to support \emph{extractors} \cite{burak06mop}in {\purescala}. Extractors are user
+We would like to support \emph{extractors} \cite{burak06mop} in {\purescala}. Extractors are user
 defined functions to perform pattern-matching on recursive data types using a
 different construction mechanism that the standard one consisting on matching
 on the constructor arguments. To use a different terminology, they provide a