--- a/Quotient-Paper/Paper.thy	Thu Oct 14 17:32:06 2010 +0100
+++ b/Quotient-Paper/Paper.thy	Fri Oct 15 15:24:19 2010 +0900
@@ -57,6 +57,11 @@
   Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
 *}
 
+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: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset])
+
 (*>*)