--- 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]