--- a/Nominal/Ex/Foo2.thy	Mon Nov 29 05:10:02 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Mon Nov 29 05:17:41 2010 +0000
@@ -127,6 +127,25 @@
 apply(auto)
 done
 
+lemma abs_rename_res:
+  fixes x::"'a::fs"
+  assumes "(p \<bullet> bs) \<sharp>* x" "(p \<bullet> bs) \<sharp>* bs" "finite bs"
+  shows "\<exists>y. [bs]res. x = [p \<bullet> bs]res. y"
+using yy assms
+apply -
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="bs" in meta_spec)
+apply(auto simp add: yy1)
+apply(rule_tac x="q \<bullet> x" in exI)
+apply(subgoal_tac "(q \<bullet> ([bs]res. x)) = [bs]res. x")
+apply(simp)
+apply(rule supp_perm_eq)
+apply(rule fresh_star_supp_conv)
+apply(simp add: fresh_star_def)
+apply(simp add: Abs_fresh_iff)
+apply(auto)
+done
+
 lemma zz0:
   assumes "p \<bullet> bs = q \<bullet> bs"
   and a: "a \<in> set bs"