--- a/Nominal/FSet.thy	Wed Apr 14 08:35:31 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 14 08:36:54 2010 +0200
@@ -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)