--- a/Quotient-Paper/Paper.thy	Wed May 26 16:17:49 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Wed May 26 16:28:35 2010 +0200
@@ -188,7 +188,8 @@
      applied to the results for the arguments.
 
   \item For unequal type constructors, look in the quotients information
-    for a quotient type that matches, and instantiate the raw type
+    for a quotient type that matches the type constructor, and instantiate
+    the raw type
     appropriately getting back an instantiation environment. We apply
     the environment to the arguments and recurse composing it with the
     aggregate map function.
@@ -235,21 +236,41 @@
   Given an aggregate raw type and quotient type:
 
   \begin{itemize}
-  \item ...
+  \item For equal types or free type variables return equality
+
+  \item For equal type constructors use the appropriate rel
+    function applied to the results for the argument pairs
+
+  \item For unequal type constructors, look in the quotients information
+    for a quotient type that matches the type constructor, and instantiate
+    the type appropriately getting back an instantiation environment. We
+    apply the environment to the arguments and recurse composing it with
+    the aggregate relation function.
+
   \end{itemize}
 
+  Again, the the behaviour of our algorithm in the last situation is
+  novel, so lets look at the example of respectfullness for @{term concat}:
+
+  @{thm concat_rsp}
+
+  This means...
+
+*}
+
+subsection {* Preservation *}
+
+section {* Lifting Theorems *}
+
+text{*
   Aggregate @{term "Rep"} and @{term "Abs"} functions are also
   present in composition quotients. An example composition quotient
   theorem that needs to be proved is the one needed to lift theorems
   about concat:
 
   @{thm quotient_compose_list[no_vars]}
-
-  Prs
 *}
 
-section {* Lifting Theorems *}
-
 text {* TBD *}
 
 text {* Why providing a statement to prove is necessary is some cases *}