diff -r 1f613b24fff8 -r a3ef7fba983f Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 30 15:07:42 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 15:09:26 2010 +0200
@@ -854,7 +854,7 @@
   of term-calculi. 
 *}
 
-section {* Alpha-Equivalence and Free Variables *}
+section {* Alpha-Equivalence and Free Variables\label{sec:alpha} *}
 
 text {*
   Our choice of syntax for specifications of term-calculi is influenced by the existing
@@ -1269,7 +1269,40 @@
 
 *}
 
-section {* The Lifting of Definitions and Properties *} 
+section {* The Lifting of Definitions and Properties *}
+
+text {*
+  To define quotient types of the raw types we first show that the defined relation
+  in an equivalence relation.
+
+  \begin{lemma} The relations $\approx_1,\ldots,\approx_n,\approx_{bn1},\ldots,\approx_{bnm}$
+  defined as above are equivalence relations.
+  \end{lemma}
+  \begin{proof}
+  Reflexivity by induction on the raw datatype, symmetry and transitivity by
+  induction on the alpha equivalence relation. Using lemma \ref{alphaeq}, the
+  conditions follow by simple calculations.
+  \end{proof}
+
+  \noindent We then define the quotient types @{text "ty\<^isub>1\<^isup>\<alpha> \<dots> ty\<^isub>n\<^isup>\<alpha>"}. To lift the raw
+  definitions to the quotient type, we need to prove that they \emph{respect} the
+  relation. We follow the definition of respectfullness given by
+  Homeier~\cite{Homeier05}. The intuition behind a respectfullness condition is that
+  when a function (or constructor) is given arguments that are alpha-equivalent the
+  results are also alpha equivalent. For arguments that are not of any of the relations
+  taken into account, equvalence is replaced by equality.
+
+% Could be written as a \{lemma}
+  In particular the respectfullness condition for a @{text "bn"} function means that for
+  alpha equivalent raw terms it returns the same bound names. Thanks to the
+  restrictions on the binding functions introduced in Section~\ref{sec:alpha}, we can
+  show that are respectful. With this we can show the respectfullness of @{text "fv_ty"}
+  functions by induction. Respectfullness of permutations is a direct consequence
+  of equivariance. Respectfullness of type constructors and of @{text "alpha_bn"} follows
+  by induction from type definitions.
+
+
+*}
 
 text {*
   Restrictions