--- a/Nominal/Nominal2_Base.thy	Thu Nov 10 01:15:19 2011 +0000
+++ b/Nominal/Nominal2_Base.thy	Sat Nov 26 09:24:19 2011 +0000
@@ -906,6 +906,11 @@
   unfolding image_def
   by (perm_simp) (rule refl)
 
+lemma Image_eqvt [eqvt]:
+  shows "p \<bullet> (R `` A) = (p \<bullet> R) `` (p \<bullet> A)"
+  unfolding Image_def
+  by (perm_simp) (rule refl)
+
 lemma UNIV_eqvt [eqvt]:
   shows "p \<bullet> UNIV = UNIV"
   unfolding UNIV_def