diff -r c6116722b44d -r 05843094273e Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 30 17:00:34 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 17:52:16 2010 +0200
@@ -1346,16 +1346,37 @@
   support in lifted theorems, since it does not preserve the relation.
   Indeed, take the term @{text "\<lambda>x. x"}. The support of the term is empty @{term "{}"},
   since the @{term "x"} is bound. On the raw level, before the binding is
-  introduced the term has the support equal to @{text "{x}"}.
+  introduced the term has the support equal to @{text "{x}"}. 
 
-  We will now show that the quotient types have a finite support.
+  To show the support equations for the lifted types we want to use the
+  Lemma \ref{suppabs}, so we start with showing that they have a finite
+  support.
 
-
+  \begin{lemma} The types @{text "ty\<^isup>\<alpha>\<^isub>1 \<dots> ty\<^isup>\<alpha>\<^isub>n"} have finite support.
+  \end{lemma}
+  \begin{proof}
+  By induction on the lifted types. For each constructor its support is
+  supported by the union of the supports of all arguments. By induction
+  hypothesis we know that each of the recursive arguments has finite
+  support. We also know that atoms and finite atom sets and lists that
+  occur in the constructors have finite support. A union of finite
+  sets is finite thus the support of the constructor is finite.
+  \end{proof}
 
-
+  \begin{lemma} For each lifted type @{text "ty\<^isup>\<alpha>\<^isub>i"}, for every @{text "x"}
+   of this type:
+  \begin{center}
+  @{term "supp x = fv_ty\<^isup>\<alpha>\<^isub>i x"}.
+  \end{center}
+  \end{lemma}
+  \begin{proof}
+  By induction on the lifted types, together with the equations that characterize
+  @{term "fv_bn"} in terms of @{term "supp"}...
+  \end{proof}
 *}
 
 text {*
+%%% FIXME: The restricions should have already been described in previous sections?
   Restrictions
 
   \begin{itemize}