--- a/Nominal/Nominal2_Eqvt.thy	Mon Feb 07 16:00:24 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Wed Feb 16 14:03:26 2011 +0000
@@ -260,6 +260,21 @@
   by (induct xs)
      (auto simp add: supp_Nil supp_Cons supp_atom)
 
+lemma filter_eqvt[eqvt]:
+  shows "p \<bullet> (filter f xs) = filter (p \<bullet> f) (p \<bullet> xs)"
+apply(induct xs)
+apply(simp)
+apply(simp only: filter.simps permute_list.simps if_eqvt)
+apply(simp only: permute_fun_app_eq)
+done
+
+lemma distinct_eqvt[eqvt]:
+  shows "p \<bullet> (distinct xs) = distinct (p \<bullet> xs)"
+apply(induct xs)
+apply(simp add: permute_bool_def)
+apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
+done
+
 
 subsection {* Equivariance Finite-Set Operations *}