--- a/Nominal/FSet.thy	Thu May 27 11:21:37 2010 +0200
+++ b/Nominal/FSet.thy	Thu May 27 14:30:07 2010 +0200
@@ -626,6 +626,11 @@
   apply auto
   done
 
+lemma insert_preserve2:
+  shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) =
+         (id ---> rep_fset ---> abs_fset) op #"
+  by (simp add: expand_fun_eq abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
+
 lemma [quot_preserve]:
   "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert"
   by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset]

--- 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 *}