--- a/Nominal/Nominal2_Base.thy	Mon Nov 15 20:54:01 2010 +0000
+++ b/Nominal/Nominal2_Base.thy	Sun Nov 21 02:17:19 2010 +0000
@@ -1579,6 +1579,15 @@
 apply(auto simp add: fresh_star_def)
 done
 
+lemma at_set_avoiding3:
+  assumes "finite xs"
+  and     "finite (supp c)" "finite (supp x)"
+  and     "xs \<sharp>* x"
+  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> x = p \<bullet> x"
+using at_set_avoiding2[OF assms]
+by (auto simp add: supp_perm_eq)
+
+
 lemma at_set_avoiding2_atom:
   assumes "finite (supp c)" "finite (supp x)"
   and     b: "a \<sharp> x"