--- a/Nominal/ExCoreHaskell.thy	Thu Mar 25 14:24:06 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Thu Mar 25 14:31:51 2010 +0100
@@ -172,9 +172,40 @@
   apply(simp add: eqvts)
   done
 
+lemma alpha_perm_bn1:
+ " alpha_bv_tvtk tvtk_lst (permute_bv_tvtk q tvtk_lst)"
+ "alpha_bv_tvck tvck_lst (permute_bv_tvck q tvck_lst)"
+ "alpha_bv_vt vt_lst (permute_bv_vt q vt_lst)"
+  apply(induct tvtk_lst rule: inducts(11))
+  apply(simp_all add:permute_bv eqvts eq_iff)
+  apply(induct tvck_lst rule: inducts(12))
+  apply(simp_all add:permute_bv eqvts eq_iff)
+  apply(induct vt_lst rule: inducts(10))
+  apply(simp_all add:permute_bv eqvts eq_iff)
+  done
+
+lemma alpha_perm_bn:
+  "alpha_bv pat (permute_bv q pat)"
+  apply(induct pat rule: inducts(9))
+  apply(simp_all add:permute_bv eqvts eq_iff alpha_perm_bn1)
+  done
+
 lemma ACons_subst:
   "supp (Abs (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"
-sorry
+  apply (simp only: eq_iff)
+  apply (rule_tac x="q" in exI)
+  apply (simp add: alphas)
+  apply (simp add: perm_bv2[symmetric])
+  apply (simp add: eqvts[symmetric])
+  apply (simp add: supp_Abs)
+  apply (simp add: fv_supp)
+  apply (simp add: alpha_perm_bn)
+  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 permute_bv_zero1:
   "permute_bv_tvck 0 b = b"