diff -r 0c1dcdefb515 -r 74637f186af7 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Thu May 27 11:21:37 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Thu May 27 14:30:07 2010 +0200
@@ -295,6 +295,19 @@
   To be able to lift theorems that talk about constants that are not
   lifted but whose type changes when lifting is performed additionally
   preservation theorems are needed.
+
+  To lift theorems that talk about insertion in lists of lifted types
+  we need to know that for any quotient type with the abstraction and
+  representation functions @{text "Abs"} and @{text Rep} we have:
+
+  @{thm [display] (concl) cons_prs[no_vars]}
+
+  This is not enough to lift theorems that talk about quotient compositions.
+  For some constants (for example empty list) it is possible to show a
+  general compositional theorem, but for @{term "op #"} it is necessary
+  to show that it respects the particular quotient type:
+
+  @{thm [display] insert_preserve2[no_vars]}
 *}
 
 subsection {* Composition of Quotient theorems *}