--- a/Nominal/Nominal2_Base_Exec.thy	Fri Mar 30 13:39:15 2012 +0200
+++ b/Nominal/Nominal2_Base_Exec.thy	Fri Mar 30 13:56:36 2012 +0200
@@ -929,6 +929,14 @@
   unfolding Inter_eq 
   by (perm_simp) (rule refl)
 
+lemma foldr_eqvt[eqvt]:
+  "p \<bullet> foldr a b c = foldr (p \<bullet> a) (p \<bullet> b) (p \<bullet> c)"
+  apply (induct b)
+  apply simp_all
+  apply (perm_simp)
+  apply simp
+  done
+
 (* FIXME: eqvt attribute *)
 lemma Sigma_eqvt:
   shows "(p \<bullet> (X \<times> Y)) = (p \<bullet> X) \<times> (p \<bullet> Y)"