--- a/Nominal/Nominal2_Eqvt.thy	Wed Feb 16 14:03:26 2011 +0000
+++ b/Nominal/Nominal2_Eqvt.thy	Wed Feb 16 14:44:33 2011 +0000
@@ -275,6 +275,10 @@
 apply(simp add: conj_eqvt Not_eqvt mem_eqvt set_eqvt)
 done
 
+lemma length_eqvt[eqvt]:
+  shows "p \<bullet> (length xs) = length (p \<bullet> xs)"
+by (induct xs) (simp_all add: permute_pure)
+
 
 subsection {* Equivariance Finite-Set Operations *}