--- a/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 28 07:27:28 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Wed Apr 28 08:22:20 2010 +0200
@@ -152,12 +152,6 @@
   unfolding vimage_def permute_fun_def [where f=f]
   unfolding Collect_eqvt2 mem_eqvt ..
 
-lemma image_eqvt:
-  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
-  unfolding permute_set_eq_image
-  unfolding permute_fun_def [where f=f]
-  by (simp add: image_image)
-
 lemma finite_permute_iff:
   shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
   unfolding permute_set_eq_vimage