--- a/Nominal/FSet.thy	Wed Apr 14 10:29:34 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 14 10:29:56 2010 +0200
@@ -245,9 +245,9 @@
   "x # x # xs \<approx> x # xs"
   by auto
 
-lemma none_mem_nil:
-  "(\<forall>x. x \<notin> set xs) = (xs \<approx> [])"
-  by simp
+lemma none_memb_nil:
+  "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])"
+  by (simp add: memb_def)
 
 lemma fset_raw_strong_cases:
   "(xs = []) \<or> (\<exists>x ys. ((\<not> memb x ys) \<and> (xs \<approx> x # ys)))"
@@ -278,6 +278,10 @@
   "memb x (delete_raw xs y) = (memb x xs \<and> x \<noteq> y)"
   by (induct xs arbitrary: x y) (auto simp add: memb_def)
 
+lemma delete_raw_rsp:
+  "l \<approx> r \<Longrightarrow> delete_raw l x \<approx> delete_raw r x"
+  by (simp add: memb_def[symmetric] memb_delete_raw)
+
 lemma [quot_respect]:
   "(op \<approx> ===> op = ===> op \<approx>) delete_raw delete_raw"
   by (simp add: memb_def[symmetric] memb_delete_raw)
@@ -339,7 +343,7 @@
 lemma ffold_raw_rsp_pre:
   "\<forall>e. memb e a = memb e b \<Longrightarrow> ffold_raw f z a = ffold_raw f z b"
   apply (induct a arbitrary: b)
-  apply (simp add: hd_in_set memb_absorb memb_def none_mem_nil)
+  apply (simp add: hd_in_set memb_absorb memb_def none_memb_nil)
   apply (simp add: ffold_raw.simps)
   apply (rule conjI)
   apply (rule_tac [!] impI)
@@ -479,15 +483,13 @@
   "fset_to_set (finsert (h :: 'a) t) = insert h (fset_to_set t)"
   by (lifting set.simps)
 
-thm memb_def[symmetric, THEN meta_eq_to_obj_eq]
-
 lemma in_fset_to_set:
   "x \<in> fset_to_set S \<equiv> x |\<in>| S"
   by (lifting memb_def[symmetric])
 
 lemma none_fin_fempty:
-  "(\<forall>x. x \<notin> fset_to_set S) = (S = {||})"
-  by (lifting none_mem_nil)
+  "(\<forall>x. x |\<notin>| S) = (S = {||})"
+  by (lifting none_memb_nil)
 
 lemma fset_cong:
   "(fset_to_set S = fset_to_set T) = (S = T)"