--- a/Nominal/ExLet.thy	Thu Mar 25 11:01:22 2010 +0100
+++ b/Nominal/ExLet.thy	Thu Mar 25 11:10:15 2010 +0100
@@ -49,9 +49,11 @@
   "permute_bn (p + q) a = permute_bn p (permute_bn q a)"
   oops
 
-lemma Lt_subst:
-  "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
-  sorry
+lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)"
+  apply(induct lts rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:test eqvts trm_lts.eq_iff)
+  done
 
 lemma perm_bn:
   "p \<bullet> bn l = bn(permute_bn p l)"
@@ -60,6 +62,24 @@
   apply(simp_all add:test eqvts)
   done
 
+lemma Lt_subst:
+  "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
+  apply (simp only: trm_lts.eq_iff)
+  apply (rule_tac x="q" in exI)
+  apply (simp add: alphas)
+  apply (simp add: permute_bn_alpha_bn)
+  apply (simp add: perm_bn[symmetric])
+  apply (simp add: eqvts[symmetric])
+  apply (simp add: supp_Abs)
+  apply (simp add: trm_lts.supp)
+  apply (rule supp_perm_eq[symmetric])
+  apply (subst supp_finite_atom_set)
+  apply (rule finite_Diff)
+  apply (simp add: finite_supp)
+  apply (assumption)
+  done
+
+
 lemma fin_bn:
   "finite (bn l)"
   apply(induct l rule: trm_lts.inducts(2))