--- a/Nominal/Ex/Foo1.thy	Mon Nov 15 20:54:01 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Sun Nov 21 02:17:19 2010 +0000
@@ -127,6 +127,30 @@
 done
 
 
+lemma Let1_rename:
+  assumes "supp ([bn1 assn]lst. trm) \<sharp>* p"
+  shows "Let1 assn trm = Let1 (permute_bn1 p assn) (p \<bullet> trm)"
+using assms
+apply -
+apply(drule supp_perm_eq[symmetric])
+apply(simp only: permute_Abs)
+apply(simp only: tt1)
+apply(simp only: foo.eq_iff)
+apply(rule conjI)
+apply(rule refl)
+apply(rule uu1)
+done
+
+lemma Let1_rename_a:
+  fixes c::"'a::fs"
+  assumes "y =  Let1 assn trm"
+  shows "\<exists>p. (p \<bullet> (set (bn1 assn))) \<sharp>* c \<and> y = Let1 (permute_bn1 p assn) (p \<bullet> trm)"
+using assms
+apply(simp only: foo.eq_iff uu1 tt1[symmetric] permute_Abs[symmetric])
+apply(simp del: permute_Abs)
+apply(rule at_set_avoiding3)
+apply(simp_all only: finite_supp Abs_fresh_star finite_set)
+done
 
 lemma strong_exhaust1:
   fixes c::"'a::fs"
@@ -158,20 +182,12 @@
 apply(simp add: finite_supp)
 apply(simp add: finite_supp)
 apply(simp add: foo.fresh fresh_star_def)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn1 assg))) \<sharp>* c \<and> supp ([bn1 assg]lst.trm) \<sharp>* q")
+apply(drule Let1_rename_a)
 apply(erule exE)
 apply(erule conjE)
 apply(rule assms(4))
-apply(perm_simp add: tt1)
+apply(simp only: set_eqvt tt1)
 apply(assumption)
-apply(drule supp_perm_eq[symmetric])
-apply(simp add: foo.eq_iff)
-apply(simp add: tt1 uu1)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: Abs_fresh_star)
 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn2 assg))) \<sharp>* c \<and> supp ([bn2 assg]lst.trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)