diff --git a/doc/faq.rst b/doc/faq.rst
new file mode 100644
index 0000000000000000000000000000000000000000..2d9c7337bb7851330b9f273abeb31dfe7903c514
--- /dev/null
+++ b/doc/faq.rst
@@ -0,0 +1,38 @@
+.. _faq:
+
+Frequently Asked Questions
+==========================
+
+If you have a question, we suggest you post it at http://stackoverflow.com
+(ty `searching for the leon tag <http://stackoverflow.com/questions/tagged/leon?sort=newest>`_)
+or contact one of the authors of this documentation.
+
+Below we collect answers to some questions that came up.
+
+Proving properties of size
+^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+I have defined a size function on my algebraic data type.
+
+.. code-block:: scala
+
+  sealed abstract class List
+  case class Cons(head: Int, tail: List) extends List
+  case object Nil extends List
+  def size(l: List) : Int = (l match {
+    case Nil => 0
+    case Cons(_, t) => 1 + size(t)
+  }) ensuring(_ >= 0)
+
+Leon neither proves nor gives a counterexample. Why?
+
+**Answer:** You should consider using `BigInt`, which
+denotes unbounded mathematical integers, instead of `Int`,
+which denotes 32-bit integers. If you replace `Int` with
+`BigInt` in the result type of `size`, the function should
+verify. Note that algebraic data types can be arbitrarily
+large, so, if the input list had the size `Int.MaxValue + 1`
+(which is 2^32) then the addition `1 + size(t)` would wrap
+around and produce `Int.MinValue` (that is, -2^31), so the
+`ensuring` clause would not hold.
+
diff --git a/doc/gettingstarted.rst b/doc/gettingstarted.rst
index 43314261a39d0efab6667c6ee92586c2184096ab..2401d2573deca44a23b4b1f0ffa03befd0b15008 100644
--- a/doc/gettingstarted.rst
+++ b/doc/gettingstarted.rst
@@ -96,11 +96,3 @@ be used directly from the shell, see
 :ref:`installation`.  In addition to invoking `./leon --help` you
 may wish to consult :ref:`cmdlineoptions`.
 
-
-Asking Questions
-----------------
-
-We are active on http://stackoverflow.com. 
-
-Try `searching for the leon tag <http://stackoverflow.com/questions/tagged/leon?sort=newest>`_.
-
diff --git a/doc/index.rst b/doc/index.rst
index 773ef1dccd10be50d404ee07ec6f118aa8b86c17..50d958f5e42b75d4ac088b29702090a6445bcce8 100644
--- a/doc/index.rst
+++ b/doc/index.rst
@@ -15,6 +15,7 @@ Contents:
    gettingstarted
    installation
    tutorial
+   faq
    purescala
    library
    xlang
diff --git a/doc/tutorial.rst b/doc/tutorial.rst
index e51691b13cad8107c85c72efb0d0c4e6d33107f1..483a1285dbb69845c8792db9fe3f742c13c1c9bb 100644
--- a/doc/tutorial.rst
+++ b/doc/tutorial.rst
@@ -217,15 +217,16 @@ definition, expressed using Scala's **case classes**.
   case object Nil extends List
   case class Cons(head: BigInt, tail: List) extends List
 
-We can read the definition as follows: List is defined
-by applying the following two rules finitely many times:
+We can read the definition as follows: the set of lists is
+defined as the least set that satisfies them:
 
   * empty list `Nil` is a list
   * if `head` is an integer and `tail` is a `List`, then
     `Cons(head,tail)` is a `List`.
 
-A list containing elements 5, 2, and 7, in that order, can
-be written as
+Each list is constructed by applying the above two rules
+finitely many times.  A concrete list containing elements 5,
+2, and 7, in that order, is denoted
 
 .. code-block:: scala