--- a/Nominal/Ex/Let.thy	Fri Oct 01 07:11:47 2010 -0400
+++ b/Nominal/Ex/Let.thy	Mon Oct 04 07:25:37 2010 +0100
@@ -97,15 +97,19 @@
 apply(simp add: finite_supp)
 apply(simp add: finite_supp)
 apply(simp add: trm_assn.fresh fresh_star_def)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs, fv_bn assn) \<and> supp ([bn assn]lst.trm) \<sharp>* q")
+apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q")
 apply(erule exE)
 apply(erule conjE)
+apply(subgoal_tac "-q \<bullet> (\<forall>assn trm. (set (bn assn) \<sharp>* c \<and>  y = Let assn trm) \<longrightarrow> P)")
+apply(perm_simp add: trm_assn.fv_bn_eqvt)
+(* HERE *)
+
+
+
 apply(simp add: set_eqvt)
 apply(subst (asm) tt)
 apply(rule_tac assms(4))
 apply(simp add: fresh_star_prod)
-apply(erule conjE)
-apply(assumption)
 apply(simp)
 apply(simp add: trm_assn.eq_iff)
 apply(drule supp_perm_eq[symmetric])