--- a/Quotient-Paper/Paper.thy	Tue Jun 15 07:58:33 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 09:12:54 2010 +0200
@@ -365,10 +365,11 @@
   \end{definition}
 
   \noindent
-  Unfortunately, restrictions in HOL's type-system prevent us from stating
-  and proving a quotient type theorem, like Proposition \ref{funquot}, for compositions 
-  of relations. However, we can prove all instances where @{text R\<^isub>1} and 
-  @{text "R\<^isub>2"} are built up by constituent equivalence relations.
+  Unfortunately a quotient type theorem, like Proposition \ref{funquot}, for
+  the composition of any two quotients in not true (it is not even typable in
+  the HOL type system). However, we can prove useful instances for compatible
+  containers. We will show such example in Section \ref{sec:resp}.
+
 *}
 
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}
@@ -728,9 +729,12 @@
 
   Lets take again the example of @{term flat}. To be able to lift
   theorems that talk about it we provide the composition quotient
-  theorem:
+  theorem which allows quotienting inside the container:
 
-  @{thm [display, indent=10] quotient_compose_list[no_vars]}
+  If @{term R} is an equivalence relation and @{term "Quotient R Abs Rep"}
+  then
+
+  @{text [display, indent=10] "Quotient (list_rel R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (abs_fset \<circ> map Abs) (map Rep o rep_fset)"}
 
   \noindent
   this theorem will then instantiate the quotients needed in the