--- a/Nominal/Nominal2_Eqvt.thy	Thu Jan 06 13:28:04 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Thu Jan 06 13:28:19 2011 +0000
@@ -232,7 +232,27 @@
   by (induct xs) (simp_all, simp only: permute_fun_app_eq)
 
 
-subsection {* Equivariance for fsets *} 
+subsection {* Equivariance Finite-Set Operations *}
+
+lemma in_fset_eqvt[eqvt]:
+  shows "(p \<bullet> (x |\<in>| S)) = ((p \<bullet> x) |\<in>| (p \<bullet> S))"
+unfolding in_fset
+by (perm_simp) (simp)
+
+lemma union_fset_eqvt[eqvt]:
+  shows "(p \<bullet> (S |\<union>| T)) = ((p \<bullet> S) |\<union>| (p \<bullet> T))"
+by (induct S) (simp_all)
+
+lemma supp_union_fset:
+  fixes S T::"'a::fs fset"
+  shows "supp (S |\<union>| T) = supp S \<union> supp T"
+by (induct S) (auto)
+
+lemma fresh_union_fset:
+  fixes S T::"'a::fs fset"
+  shows "a \<sharp> S |\<union>| T \<longleftrightarrow> a \<sharp> S \<and> a \<sharp> T"
+unfolding fresh_def
+by (simp add: supp_union_fset)
 
 lemma map_fset_eqvt[eqvt]: 
   shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"