--- a/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 30 10:32:34 2010 +0200
+++ b/Nominal-General/Nominal2_Eqvt.thy	Fri Apr 30 14:21:18 2010 +0100
@@ -156,6 +156,16 @@
   shows "p \<bullet> {x. P x} = {x. p \<bullet> (P (-p \<bullet> x))}"
   by (perm_simp add: permute_minus_cancel) (rule refl)
 
+lemma Bex_eqvt[eqvt]:
+  shows "p \<bullet> (\<exists>x \<in> S. P x) = (\<exists>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+  unfolding Bex_def
+  by (perm_simp) (rule refl)
+
+lemma Ball_eqvt[eqvt]:
+  shows "p \<bullet> (\<forall>x \<in> S. P x) = (\<forall>x \<in> (p \<bullet> S). (p \<bullet> P) x)"
+  unfolding Ball_def
+  by (perm_simp) (rule refl)
+
 lemma empty_eqvt[eqvt]:
   shows "p \<bullet> {} = {}"
   unfolding empty_def
@@ -206,6 +216,11 @@
   unfolding vimage_def
   by (perm_simp) (rule refl)
 
+lemma Union_eqvt[eqvt]:
+  shows "p \<bullet> (\<Union> S) = \<Union> (p \<bullet> S)"
+  unfolding Union_eq 
+  by (perm_simp) (rule refl)
+
 lemma finite_permute_iff:
   shows "finite (p \<bullet> A) \<longleftrightarrow> finite A"
   unfolding permute_set_eq_vimage