--- a/Nominal/ExCoreHaskell.thy	Thu Mar 25 11:16:25 2010 +0100
+++ b/Nominal/ExCoreHaskell.thy	Thu Mar 25 11:29:54 2010 +0100
@@ -242,7 +242,7 @@
          P4 (d :: 'd :: pt) ty_lst \<and>
          P5 (e :: 'e :: {pt,fs}) co \<and>
          P6 (f :: 'f :: pt) co_lst \<and>
-         P7 (g :: 'g :: pt) trm \<and>
+         P7 (g :: 'g :: {pt,fs}) trm \<and>
          P8 (h :: 'h :: {pt,fs}) assoc_lst \<and>
          P9 (i :: 'i :: pt) pat \<and>
          P10 (j :: 'j :: pt) vt_lst \<and>
@@ -334,6 +334,47 @@
     apply (simp only: supp_Abs eqvts)
     apply blast
 
+
+(* GOAL3 a copy-and-paste of Goal2 with consts and variable names changed *)
+    apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> g \<and>
+                       supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> trm)) \<sharp>* pa)")
+    apply clarify
+    apply (simp only: perm)
+    apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)"
+               and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst)
+    apply (simp only: eq_iff)
+    apply (rule_tac x="-pa" in exI)
+    apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp)
+    apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
+                and s="pa \<bullet> (p \<bullet> supp trm - {p \<bullet> atom tvar})" in subst)
+    apply (simp add: eqvts)
+    apply (simp add: eqvts[symmetric])
+    apply (rule conjI)
+    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 (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)
+    apply (rule a29)
+    apply simp
+    apply(rotate_tac 1)
+    apply(erule_tac x="(pa + p)" in allE)
+    apply simp
+    apply (simp add: eqvts eqvts_raw)
+    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
+
 prefer 5
 (*  using a38*)
     apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (bv (p \<bullet> pat))) \<sharp>* h \<and>