--- a/Nominal/Nominal2_Eqvt.thy	Wed Jan 19 17:54:50 2011 +0100
+++ b/Nominal/Nominal2_Eqvt.thy	Wed Jan 19 18:07:29 2011 +0100
@@ -244,6 +244,16 @@
   shows "p \<bullet> (map f xs) = map (p \<bullet> f) (p \<bullet> xs)"
   by (induct xs) (simp_all, simp only: permute_fun_app_eq)
 
+lemma removeAll_eqvt[eqvt]:
+  shows "p \<bullet> (removeAll x xs) = removeAll (p \<bullet> x) (p \<bullet> xs)"
+  by (induct xs) (auto)
+
+lemma supp_removeAll:
+  fixes x::"atom"
+  shows "supp (removeAll x xs) = supp xs - {x}"
+  by (induct xs)
+     (auto simp add: supp_Nil supp_Cons supp_atom)
+
 
 subsection {* Equivariance Finite-Set Operations *}