--- a/Nominal/ExCoreHaskell.thy	Wed Mar 24 14:49:51 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Wed Mar 24 16:06:31 2010 +0100
@@ -87,6 +87,11 @@
 
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp]
+lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm
+
+lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)"
+  unfolding fresh_star_def Ball_def
+  by auto (simp_all add: fresh_minus_perm)
 
 lemma 
   assumes a01: "\<And>b. P1 b KStar"
@@ -145,7 +150,7 @@
     \<Longrightarrow> P12 b (TVCKCons tvar ckind tvck_lst)"
   shows "P1 (a :: 'a :: pt) tkind \<and>
          P2 (b :: 'b :: pt) ckind \<and>
-         P3 (c :: 'c :: pt) ty \<and>
+         P3 (c :: 'c :: {pt,fs}) ty \<and>
          P4 (d :: 'd :: pt) ty_lst \<and>
          P5 (e :: 'e :: pt) co \<and>
          P6 (f :: 'f :: pt) co_lst \<and>
@@ -160,7 +165,53 @@
     apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct)
     apply (tactic {* ALLGOALS (REPEAT o rtac allI) *})
     apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *})
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and> supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)")
+    prefer 2
+    apply (rule at_set_avoiding2_atom)
+    apply (simp add: finite_supp)
+    apply (simp add: finite_supp)
+    apply (simp add: fresh_def)
+    apply (simp only: supp_Abs eqvts)
+    apply blast
+    apply clarify
+    apply (simp only: perm)
+    apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)
+    apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff)
+    apply (rule_tac x="-pa" in exI)
+    apply (simp add: alphas)
+    prefer 2
+    apply (rule a08)
+    apply simp
+    apply(rotate_tac 1)
+    apply(erule_tac x="(pa + p)" in allE)
+    apply simp
+    apply (simp add: eqvts eqvts_raw)
+    apply (simp add: eqvts eqvts_raw supp_Abs)
+    apply (rule conjI)
+    apply (simp add: eqvts[symmetric])
+    apply (simp add: fv_supp)
+    apply (rule_tac t="pa \<bullet> p \<bullet> supp ty - {pa \<bullet> p \<bullet> atom tvar}"
+                and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
+    apply (simp add: eqvts)
+    apply (rule supp_perm_eq)
+    apply (simp add: eqvts)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts)
+    apply (simp add: fv_supp)
+    apply (simp add: eqvts[symmetric])
+    apply (rule_tac t="pa \<bullet> p \<bullet> supp ty - {pa \<bullet> p \<bullet> atom tvar}"
+                and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst)
+    apply (simp add: eqvts)
+    apply (subst supp_perm_eq)
+    apply (subst supp_finite_atom_set)
+    apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp)
+    apply (simp add: eqvts)
+    apply assumption
+    apply (simp add: fresh_star_minus_perm)
     sorry
+
   have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast
   have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast
   have g3: "P3 c (0 \<bullet> ty) \<and>