--- a/Nominal/Nominal2_Eqvt.thy	Mon Feb 07 15:59:37 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Mon Feb 07 16:00:24 2011 +0000
@@ -196,7 +196,7 @@
   unfolding psubset_eq
   by (perm_simp) (rule refl)
 
-lemma image_eqvt:
+lemma image_eqvt[eqvt]:
   shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
   unfolding permute_set_eq_image
   unfolding permute_fun_def [where f=f]
@@ -212,6 +212,12 @@
   unfolding Union_eq 
   by (perm_simp) (rule refl)
 
+lemma Sigma_eqvt:
+  shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"
+unfolding Sigma_def
+unfolding UNION_eq_Union_image
+by (perm_simp) (rule refl)
+
 lemma finite_permute_iff:
   shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
   unfolding permute_set_eq_vimage