diff --git a/src/HOL/Nominal/Examples/Crary.thy b/src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy
+++ b/src/HOL/Nominal/Examples/Crary.thy
@@ -1,964 +1,935 @@
 (*                                                    *)
 (* Formalisation of the chapter on Logical Relations  *)
 (* and a Case Study in Equivalence Checking           *)
 (* by Karl Crary from the book on Advanced Topics in  *)
 (* Types and Programming Languages, MIT Press 2005    *)
 
 (* The formalisation was done by Julien Narboux and   *)
 (* Christian Urban.                                   *)
 
 theory Crary
   imports "HOL-Nominal.Nominal"
 begin
 
 atom_decl name 
 
 nominal_datatype ty = 
     TBase 
   | TUnit 
   | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
 
 nominal_datatype trm = 
     Unit
   | Var "name" ("Var _" [100] 100)
   | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
   | App "trm" "trm" ("App _ _" [110,110] 100)
   | Const "nat"
 
 type_synonym Ctxt  = "(name\<times>ty) list"
 type_synonym Subst = "(name\<times>trm) list" 
 
 
 lemma perm_ty[simp]: 
   fixes T::"ty"
   and   pi::"name prm"
   shows "pi\<bullet>T = T"
   by (induct T rule: ty.induct) (simp_all)
 
 lemma fresh_ty[simp]:
   fixes x::"name" 
   and   T::"ty"
   shows "x\<sharp>T"
   by (simp add: fresh_def supp_def)
 
 lemma ty_cases:
   fixes T::ty
   shows "(\<exists> T\<^sub>1 T\<^sub>2. T=T\<^sub>1\<rightarrow>T\<^sub>2) \<or> T=TUnit \<or> T=TBase"
 by (induct T rule:ty.induct) (auto)
 
 instantiation ty :: size
 begin
 
 nominal_primrec size_ty
 where
   "size (TBase) = 1"
 | "size (TUnit) = 1"
 | "size (T\<^sub>1\<rightarrow>T\<^sub>2) = size T\<^sub>1 + size T\<^sub>2"
 by (rule TrueI)+
 
 instance ..
 
 end
 
 lemma ty_size_greater_zero[simp]:
   fixes T::"ty"
   shows "size T > 0"
 by (nominal_induct rule: ty.strong_induct) (simp_all)
 
 section \<open>Substitutions\<close>
 
 fun
   lookup :: "Subst \<Rightarrow> name \<Rightarrow> trm"   
 where
   "lookup [] x        = Var x"
 | "lookup ((y,T)#\<theta>) x = (if x=y then T else lookup \<theta> x)"
 
 lemma lookup_eqvt[eqvt]:
   fixes pi::"name prm"
   shows "pi\<bullet>(lookup \<theta> x) = lookup (pi\<bullet>\<theta>) (pi\<bullet>x)"
-by (induct \<theta>) (auto simp add: perm_bij)
+by (induct \<theta>) (auto simp: perm_bij)
 
 lemma lookup_fresh:
   fixes z::"name"
   assumes a: "z\<sharp>\<theta>" "z\<sharp>x"
   shows "z\<sharp> lookup \<theta> x"
 using a
 by (induct rule: lookup.induct) 
-   (auto simp add: fresh_list_cons)
+   (auto simp: fresh_list_cons)
 
 lemma lookup_fresh':
   assumes a: "z\<sharp>\<theta>"
   shows "lookup \<theta> z = Var z"
 using a
 by (induct rule: lookup.induct)
-   (auto simp add: fresh_list_cons fresh_prod fresh_atm)
+   (auto simp: fresh_list_cons fresh_prod fresh_atm)
  
 nominal_primrec
   psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [100,100] 130)
 where
   "\<theta><(Var x)> = (lookup \<theta> x)"
 | "\<theta><(App t\<^sub>1 t\<^sub>2)> = App \<theta><t\<^sub>1> \<theta><t\<^sub>2>"
 | "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)"
 | "\<theta><(Const n)> = Const n"
 | "\<theta><(Unit)> = Unit"
-apply(finite_guess)+
-apply(rule TrueI)+
-apply(simp add: abs_fresh)+
-apply(fresh_guess)+
-done
+  by(finite_guess | simp add: abs_fresh | fresh_guess)+
 
 abbreviation 
  subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100)
 where
   "t[x::=t']  \<equiv> ([(x,t')])<t>" 
 
 lemma subst[simp]:
   shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
   and   "(App t\<^sub>1 t\<^sub>2)[y::=t'] = App (t\<^sub>1[y::=t']) (t\<^sub>2[y::=t'])"
   and   "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
   and   "Const n[y::=t'] = Const n"
   and   "Unit [y::=t'] = Unit"
   by (simp_all add: fresh_list_cons fresh_list_nil)
 
 lemma subst_eqvt[eqvt]:
   fixes pi::"name prm" 
   shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]"
   by (nominal_induct t avoiding: x t' rule: trm.strong_induct)
      (perm_simp add: fresh_bij)+
 
 lemma subst_rename: 
   fixes c::"name"
   assumes a: "c\<sharp>t\<^sub>1"
   shows "t\<^sub>1[a::=t\<^sub>2] = ([(c,a)]\<bullet>t\<^sub>1)[c::=t\<^sub>2]"
 using a
-apply(nominal_induct t\<^sub>1 avoiding: a c t\<^sub>2 rule: trm.strong_induct)
-apply(simp add: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)+
-done
+  by (nominal_induct t\<^sub>1 avoiding: a c t\<^sub>2 rule: trm.strong_induct)
+     (auto simp: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)
 
 lemma fresh_psubst: 
   fixes z::"name"
   assumes a: "z\<sharp>t" "z\<sharp>\<theta>"
   shows "z\<sharp>(\<theta><t>)"
 using a
 by (nominal_induct t avoiding: z \<theta> t rule: trm.strong_induct)
-   (auto simp add: abs_fresh lookup_fresh)
+   (auto simp: abs_fresh lookup_fresh)
 
 lemma fresh_subst'':
   fixes z::"name"
   assumes "z\<sharp>t\<^sub>2"
   shows "z\<sharp>t\<^sub>1[z::=t\<^sub>2]"
 using assms 
 by (nominal_induct t\<^sub>1 avoiding: t\<^sub>2 z rule: trm.strong_induct)
-   (auto simp add: abs_fresh fresh_nat fresh_atm)
+   (auto simp: abs_fresh fresh_nat fresh_atm)
 
 lemma fresh_subst':
   fixes z::"name"
   assumes "z\<sharp>[y].t\<^sub>1" "z\<sharp>t\<^sub>2"
   shows "z\<sharp>t\<^sub>1[y::=t\<^sub>2]"
 using assms 
 by (nominal_induct t\<^sub>1 avoiding: y t\<^sub>2 z rule: trm.strong_induct)
-   (auto simp add: abs_fresh fresh_nat fresh_atm)
+   (auto simp: abs_fresh fresh_nat fresh_atm)
 
 lemma fresh_subst:
   fixes z::"name"
   assumes a: "z\<sharp>t\<^sub>1" "z\<sharp>t\<^sub>2"
   shows "z\<sharp>t\<^sub>1[y::=t\<^sub>2]"
 using a 
-by (auto simp add: fresh_subst' abs_fresh) 
+by (auto simp: fresh_subst' abs_fresh) 
 
 lemma fresh_psubst_simp:
   assumes "x\<sharp>t"
   shows "((x,u)#\<theta>)<t> = \<theta><t>" 
 using assms
 proof (nominal_induct t avoiding: x u \<theta> rule: trm.strong_induct)
   case (Lam y t x u)
   have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact+
   moreover have "x\<sharp> Lam [y].t" by fact 
   ultimately have "x\<sharp>t" by (simp add: abs_fresh fresh_atm)
   moreover have ih:"\<And>n T. n\<sharp>t \<Longrightarrow> ((n,T)#\<theta>)<t> = \<theta><t>" by fact
   ultimately have "((x,u)#\<theta>)<t> = \<theta><t>" by auto
   moreover have "((x,u)#\<theta>)<Lam [y].t> = Lam [y].(((x,u)#\<theta>)<t>)" using fs 
     by (simp add: fresh_list_cons fresh_prod)
   moreover have " \<theta><Lam [y].t> = Lam [y]. (\<theta><t>)" using fs by simp
   ultimately show "((x,u)#\<theta>)<Lam [y].t> = \<theta><Lam [y].t>" by auto
-qed (auto simp add: fresh_atm abs_fresh)
+qed (auto simp: fresh_atm abs_fresh)
 
 lemma forget: 
   fixes x::"name"
   assumes a: "x\<sharp>t" 
   shows "t[x::=t'] = t"
   using a
 by (nominal_induct t avoiding: x t' rule: trm.strong_induct)
-   (auto simp add: fresh_atm abs_fresh)
+   (auto simp: fresh_atm abs_fresh)
 
 lemma subst_fun_eq:
   fixes u::trm
   assumes h:"[x].t\<^sub>1 = [y].t\<^sub>2"
   shows "t\<^sub>1[x::=u] = t\<^sub>2[y::=u]"
 proof -
   { 
     assume "x=y" and "t\<^sub>1=t\<^sub>2"
     then have ?thesis using h by simp
   }
   moreover 
   {
     assume h1:"x \<noteq> y" and h2:"t\<^sub>1=[(x,y)] \<bullet> t\<^sub>2" and h3:"x \<sharp> t\<^sub>2"
     then have "([(x,y)] \<bullet> t\<^sub>2)[x::=u] = t\<^sub>2[y::=u]" by (simp add: subst_rename)
     then have ?thesis using h2 by simp 
   }
   ultimately show ?thesis using alpha h by blast
 qed
 
 lemma psubst_empty[simp]:
   shows "[]<t> = t"
 by (nominal_induct t rule: trm.strong_induct) 
-   (auto simp add: fresh_list_nil)
+   (auto simp: fresh_list_nil)
 
 lemma psubst_subst_psubst:
   assumes h:"c\<sharp>\<theta>"
   shows "\<theta><t>[c::=s] = ((c,s)#\<theta>)<t>"
   using h
 by (nominal_induct t avoiding: \<theta> c s rule: trm.strong_induct)
-   (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst)
+   (auto simp: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst)
 
 lemma subst_fresh_simp:
   assumes a: "x\<sharp>\<theta>"
   shows "\<theta><Var x> = Var x"
 using a
-by (induct \<theta> arbitrary: x) (auto simp add:fresh_list_cons fresh_prod fresh_atm)
+by (induct \<theta> arbitrary: x) (auto simp:fresh_list_cons fresh_prod fresh_atm)
 
 lemma psubst_subst_propagate: 
   assumes "x\<sharp>\<theta>" 
   shows "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]"
 using assms
 proof (nominal_induct t avoiding: x u \<theta> rule: trm.strong_induct)
   case (Var n x u \<theta>)
   { assume "x=n"
     moreover have "x\<sharp>\<theta>" by fact 
     ultimately have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using subst_fresh_simp by auto
   }
   moreover 
   { assume h:"x\<noteq>n"
-    then have "x\<sharp>Var n" by (auto simp add: fresh_atm) 
+    then have "x\<sharp>Var n" by (auto simp: fresh_atm) 
     moreover have "x\<sharp>\<theta>" by fact
     ultimately have "x\<sharp>\<theta><Var n>" using fresh_psubst by blast
     then have " \<theta><Var n>[x::=\<theta><u>] =  \<theta><Var n>" using forget by auto
     then have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using h by auto
   }
   ultimately show ?case by auto  
 next
   case (Lam n t x u \<theta>)
   have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact+
   have ih:"\<And> y s \<theta>. y\<sharp>\<theta> \<Longrightarrow> ((\<theta><(t[y::=s])>) = ((\<theta><t>)[y::=(\<theta><s>)]))" by fact
   have "\<theta> <(Lam [n].t)[x::=u]> = \<theta><Lam [n]. (t [x::=u])>" using fs by auto
   then have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n]. \<theta><t [x::=u]>" using fs by auto
   moreover have "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]" using ih fs by blast
   ultimately have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n].(\<theta><t>[x::=\<theta><u>])" by auto
   moreover have "Lam [n].(\<theta><t>[x::=\<theta><u>]) = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs fresh_psubst by auto
   ultimately have "\<theta><(Lam [n].t)[x::=u]> = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs by auto
   then show "\<theta><(Lam [n].t)[x::=u]> = \<theta><Lam [n].t>[x::=\<theta><u>]" using fs by auto
 qed (auto)
 
 section \<open>Typing\<close>
 
 inductive
   valid :: "Ctxt \<Rightarrow> bool"
 where
   v_nil[intro]:  "valid []"
 | v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,T)#\<Gamma>)"
 
 equivariance valid 
 
 inductive_cases
   valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)"
 
 abbreviation
   "sub_context" :: "Ctxt \<Rightarrow> Ctxt \<Rightarrow> bool" (" _ \<subseteq> _ " [55,55] 55)
 where
   "\<Gamma>\<^sub>1 \<subseteq> \<Gamma>\<^sub>2 \<equiv> \<forall>a T. (a,T)\<in>set \<Gamma>\<^sub>1 \<longrightarrow> (a,T)\<in>set \<Gamma>\<^sub>2"
 
 lemma valid_monotonicity[elim]:
  fixes \<Gamma> \<Gamma>' :: Ctxt
  assumes a: "\<Gamma> \<subseteq> \<Gamma>'" 
  and     b: "x\<sharp>\<Gamma>'"
  shows "(x,T\<^sub>1)#\<Gamma> \<subseteq> (x,T\<^sub>1)#\<Gamma>'"
 using a b by auto
 
 lemma fresh_context: 
   fixes  \<Gamma> :: "Ctxt"
   and    a :: "name"
   assumes "a\<sharp>\<Gamma>"
   shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"
 using assms 
 by (induct \<Gamma>)
-   (auto simp add: fresh_prod fresh_list_cons fresh_atm)
+   (auto simp: fresh_prod fresh_list_cons fresh_atm)
 
 lemma type_unicity_in_context:
   assumes a: "valid \<Gamma>" 
   and     b: "(x,T\<^sub>1) \<in> set \<Gamma>" 
   and     c: "(x,T\<^sub>2) \<in> set \<Gamma>"
   shows "T\<^sub>1=T\<^sub>2"
 using a b c
 by (induct \<Gamma>)
    (auto dest!: fresh_context)
 
 inductive
   typing :: "Ctxt\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 
 where
   T_Var[intro]:   "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
 | T_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> e\<^sub>1 : T\<^sub>1\<rightarrow>T\<^sub>2; \<Gamma> \<turnstile> e\<^sub>2 : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App e\<^sub>1 e\<^sub>2 : T\<^sub>2"
 | T_Lam[intro]:   "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^sub>1)#\<Gamma> \<turnstile> t : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^sub>1\<rightarrow>T\<^sub>2"
 | T_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase"
 | T_Unit[intro]:  "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit"
 
 equivariance typing
 
 nominal_inductive typing
   by (simp_all add: abs_fresh)
 
 lemma typing_implies_valid:
   assumes a: "\<Gamma> \<turnstile> t : T"
   shows "valid \<Gamma>"
   using a by (induct) (auto)
 
 declare trm.inject [simp add]
 declare ty.inject  [simp add]
 
 inductive_cases typing_inv_auto[elim]:
   "\<Gamma> \<turnstile> Lam [x].t : T"
   "\<Gamma> \<turnstile> Var x : T"
   "\<Gamma> \<turnstile> App x y : T"
   "\<Gamma> \<turnstile> Const n : T"
   "\<Gamma> \<turnstile> Unit : TUnit"
   "\<Gamma> \<turnstile> s : TUnit"
 
 declare trm.inject [simp del]
 declare ty.inject [simp del]
 
 
 section \<open>Definitional Equivalence\<close>
 
 inductive
   def_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<equiv> _ : _" [60,60] 60) 
 where
   Q_Refl[intro]:  "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<equiv> t : T"
 | Q_Symm[intro]:  "\<Gamma> \<turnstile> t \<equiv> s : T \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"
 | Q_Trans[intro]: "\<lbrakk>\<Gamma> \<turnstile> s \<equiv> t : T; \<Gamma> \<turnstile> t \<equiv> u : T\<rbrakk> \<Longrightarrow>  \<Gamma> \<turnstile> s \<equiv> u : T"
 | Q_Abs[intro]:   "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^sub>1)#\<Gamma> \<turnstile> s\<^sub>2 \<equiv> t\<^sub>2 : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x]. s\<^sub>2 \<equiv>  Lam [x]. t\<^sub>2 : T\<^sub>1 \<rightarrow> T\<^sub>2"
 | Q_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> s\<^sub>1 \<equiv> t\<^sub>1 : T\<^sub>1 \<rightarrow> T\<^sub>2 ; \<Gamma> \<turnstile> s\<^sub>2 \<equiv> t\<^sub>2 : T\<^sub>1\<rbrakk> \<Longrightarrow>  \<Gamma> \<turnstile> App s\<^sub>1 s\<^sub>2 \<equiv> App t\<^sub>1 t\<^sub>2 : T\<^sub>2"
 | Q_Beta[intro]:  "\<lbrakk>x\<sharp>(\<Gamma>,s\<^sub>2,t\<^sub>2); (x,T\<^sub>1)#\<Gamma> \<turnstile> s\<^sub>1 \<equiv> t\<^sub>1 : T\<^sub>2 ; \<Gamma> \<turnstile> s\<^sub>2 \<equiv> t\<^sub>2 : T\<^sub>1\<rbrakk> 
                    \<Longrightarrow>  \<Gamma> \<turnstile> App (Lam [x]. s\<^sub>1) s\<^sub>2 \<equiv> t\<^sub>1[x::=t\<^sub>2] : T\<^sub>2"
 | Q_Ext[intro]:   "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^sub>2\<rbrakk> 
                    \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T\<^sub>1 \<rightarrow> T\<^sub>2"
 | Q_Unit[intro]:  "\<lbrakk>\<Gamma> \<turnstile> s : TUnit; \<Gamma> \<turnstile> t: TUnit\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : TUnit"
 
 equivariance def_equiv
 
 nominal_inductive def_equiv
   by (simp_all add: abs_fresh fresh_subst'')
 
 lemma def_equiv_implies_valid:
   assumes a: "\<Gamma> \<turnstile> t \<equiv> s : T"
   shows "valid \<Gamma>"
 using a by (induct) (auto elim: typing_implies_valid)
 
 section \<open>Weak Head Reduction\<close>
 
 inductive
   whr_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<leadsto> _" [80,80] 80) 
 where
   QAR_Beta[intro]: "App (Lam [x]. t\<^sub>1) t\<^sub>2 \<leadsto> t\<^sub>1[x::=t\<^sub>2]"
 | QAR_App[intro]:  "t\<^sub>1 \<leadsto> t\<^sub>1' \<Longrightarrow> App t\<^sub>1 t\<^sub>2 \<leadsto> App t\<^sub>1' t\<^sub>2"
 
 declare trm.inject  [simp add]
 declare ty.inject  [simp add]
 
 inductive_cases whr_inv_auto[elim]: 
   "t \<leadsto> t'"
   "Lam [x].t \<leadsto> t'"
   "App (Lam [x].t12) t2 \<leadsto> t"
   "Var x \<leadsto> t"
   "Const n \<leadsto> t"
   "App p q \<leadsto> t"
   "t \<leadsto> Const n"
   "t \<leadsto> Var x"
   "t \<leadsto> App p q"
 
 declare trm.inject  [simp del]
 declare ty.inject  [simp del]
 
 equivariance whr_def
 
 section \<open>Weak Head Normalisation\<close>
 
 abbreviation 
  nf :: "trm \<Rightarrow> bool" ("_ \<leadsto>|" [100] 100)
 where
   "t\<leadsto>|  \<equiv> \<not>(\<exists> u. t \<leadsto> u)" 
 
 inductive
   whn_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) 
 where
   QAN_Reduce[intro]: "\<lbrakk>s \<leadsto> t; t \<Down> u\<rbrakk> \<Longrightarrow> s \<Down> u"
 | QAN_Normal[intro]: "t\<leadsto>|  \<Longrightarrow> t \<Down> t"
 
 declare trm.inject[simp]
 
 inductive_cases whn_inv_auto[elim]: "t \<Down> t'"
 
 declare trm.inject[simp del]
 
 equivariance whn_def
 
 lemma red_unicity : 
   assumes a: "x \<leadsto> a" 
   and     b: "x \<leadsto> b"
   shows "a=b"
   using a b
-apply (induct arbitrary: b)
-apply (erule whr_inv_auto(3))
-apply (clarify)
-apply (rule subst_fun_eq)
-apply (simp)
-apply (force)
-apply (erule whr_inv_auto(6))
-apply (blast)+
-done
+by (induct arbitrary: b) (use subst_fun_eq in blast)+
 
 lemma nf_unicity :
   assumes "x \<Down> a" and "x \<Down> b"
   shows "a=b"
   using assms 
 proof (induct arbitrary: b)
   case (QAN_Reduce x t a b)
   have h:"x \<leadsto> t" "t \<Down> a" by fact+
   have ih:"\<And>b. t \<Down> b \<Longrightarrow> a = b" by fact
-  have "x \<Down> b" by fact
-  then obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> b" using h by auto
+  obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> b" using h \<open>x \<Down> b\<close> by auto
   then have "t=t'" using h red_unicity by auto
   then show "a=b" using ih hl by auto
 qed (auto)
 
 
 section \<open>Algorithmic Term Equivalence and Algorithmic Path Equivalence\<close>
 
 inductive
   alg_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<Leftrightarrow> _ : _" [60,60,60,60] 60) 
 and
   alg_path_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60,60,60] 60) 
 where
   QAT_Base[intro]:  "\<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase"
 | QAT_Arrow[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^sub>2\<rbrakk> 
                      \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1 \<rightarrow> T\<^sub>2"
 | QAT_One[intro]:   "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : TUnit"
 | QAP_Var[intro]:   "\<lbrakk>valid \<Gamma>;(x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T"
 | QAP_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^sub>1 \<rightarrow> T\<^sub>2; \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T\<^sub>2"
 | QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase"
 
 equivariance alg_equiv
 
 nominal_inductive alg_equiv
   avoids QAT_Arrow: x
   by simp_all
 
 declare trm.inject [simp add]
 declare ty.inject  [simp add]
 
 inductive_cases alg_equiv_inv_auto[elim]: 
   "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
   "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^sub>1 \<rightarrow> T\<^sub>2"
   "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase"
   "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit"
   "\<Gamma> \<turnstile> s\<leftrightarrow>t : T\<^sub>1 \<rightarrow> T\<^sub>2"
 
   "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T"
   "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'"
   "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T"
   "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'"
   "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T"
   "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T"
   "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T"
   "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T"
   "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T"
   "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T"
 
 declare trm.inject [simp del]
 declare ty.inject [simp del]
 
 lemma Q_Arrow_strong_inversion:
   assumes fs: "x\<sharp>\<Gamma>" "x\<sharp>t" "x\<sharp>u" 
   and h: "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^sub>1\<rightarrow>T\<^sub>2"
   shows "(x,T\<^sub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2"
 proof -
   obtain y where fs2: "y\<sharp>(\<Gamma>,t,u)" and "(y,T\<^sub>1)#\<Gamma> \<turnstile> App t (Var y) \<Leftrightarrow> App u (Var y) : T\<^sub>2" 
     using h by auto
   then have "([(x,y)]\<bullet>((y,T\<^sub>1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) \<Leftrightarrow> [(x,y)]\<bullet> App u (Var y) : T\<^sub>2" 
     using  alg_equiv.eqvt[simplified] by blast
   then show ?thesis using fs fs2 by (perm_simp)
 qed
 
 (*
 Warning this lemma is false:
 
 lemma algorithmic_type_unicity:
   shows "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<Leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
   and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
 
 Here is the counter example : 
 \<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : Tbase and \<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : TUnit
 *)
 
 lemma algorithmic_path_type_unicity:
   shows "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<Longrightarrow> T = T'"
 proof (induct arbitrary:  u T' 
        rule: alg_equiv_alg_path_equiv.inducts(2) [of _ _ _ _ _  "%a b c d . True"    ])
   case (QAP_Var \<Gamma> x T u T')
   have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact
   then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto
   moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact+
   ultimately show "T=T'" using type_unicity_in_context by auto
 next
   case (QAP_App \<Gamma> p q T\<^sub>1 T\<^sub>2 s t u T\<^sub>2')
   have ih:"\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^sub>1\<rightarrow>T\<^sub>2 = T" by fact
   have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^sub>2'" by fact
   then obtain r t T\<^sub>1' where "u = App r t"  "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^sub>1' \<rightarrow> T\<^sub>2'" by auto
   with ih have "T\<^sub>1\<rightarrow>T\<^sub>2 = T\<^sub>1' \<rightarrow> T\<^sub>2'" by auto
   then show "T\<^sub>2=T\<^sub>2'" using ty.inject by auto
 qed (auto)
 
 lemma alg_path_equiv_implies_valid:
   shows  "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>" 
   and    "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>"
 by (induct rule : alg_equiv_alg_path_equiv.inducts) auto
 
 lemma algorithmic_symmetry:
   shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> s : T" 
   and   "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> s : T"
 by (induct rule: alg_equiv_alg_path_equiv.inducts) 
-   (auto simp add: fresh_prod)
+   (auto simp: fresh_prod)
 
 lemma algorithmic_transitivity:
   shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<Leftrightarrow> u : T \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> u : T"
   and   "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> u : T \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T"
 proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: u rule: alg_equiv_alg_path_equiv.strong_inducts)
   case (QAT_Base s p t q \<Gamma> u)
   have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : TBase" by fact
   then obtain r' q' where b1: "t \<Down> q'" and b2: "u \<Down> r'" and b3: "\<Gamma> \<turnstile> q' \<leftrightarrow> r' : TBase" by auto
   have ih: "\<Gamma> \<turnstile> q \<leftrightarrow> r' : TBase \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> r' : TBase" by fact
   have "t \<Down> q" by fact
   with b1 have eq: "q=q'" by (simp add: nf_unicity)
   with ih b3 have "\<Gamma> \<turnstile> p \<leftrightarrow> r' : TBase" by simp
   moreover
   have "s \<Down> p" by fact
   ultimately show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : TBase" using b2 by auto
 next
   case (QAT_Arrow  x \<Gamma> s t T\<^sub>1 T\<^sub>2 u)
   have ih:"(x,T\<^sub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2 
                                    \<Longrightarrow> (x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2" by fact
   have fs: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>u" by fact+
   have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^sub>1\<rightarrow>T\<^sub>2" by fact
   then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2" using fs 
     by (simp add: Q_Arrow_strong_inversion)
   with ih have "(x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^sub>2" by simp
-  then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^sub>1\<rightarrow>T\<^sub>2" using fs by (auto simp add: fresh_prod)
+  then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^sub>1\<rightarrow>T\<^sub>2" using fs by (auto simp: fresh_prod)
 next
   case (QAP_App \<Gamma> p q T\<^sub>1 T\<^sub>2 s t u)
   have "\<Gamma> \<turnstile> App q t \<leftrightarrow> u : T\<^sub>2" by fact
   then obtain r T\<^sub>1' v where ha: "\<Gamma> \<turnstile> q \<leftrightarrow> r : T\<^sub>1'\<rightarrow>T\<^sub>2" and hb: "\<Gamma> \<turnstile> t \<Leftrightarrow> v : T\<^sub>1'" and eq: "u = App r v" 
     by auto
   have ih1: "\<Gamma> \<turnstile> q \<leftrightarrow> r : T\<^sub>1\<rightarrow>T\<^sub>2 \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^sub>1\<rightarrow>T\<^sub>2" by fact
   have ih2:"\<Gamma> \<turnstile> t \<Leftrightarrow> v : T\<^sub>1 \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> v : T\<^sub>1" by fact
   have "\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^sub>1\<rightarrow>T\<^sub>2" by fact
   then have "\<Gamma> \<turnstile> q \<leftrightarrow> p : T\<^sub>1\<rightarrow>T\<^sub>2" by (simp add: algorithmic_symmetry)
   with ha have "T\<^sub>1'\<rightarrow>T\<^sub>2 = T\<^sub>1\<rightarrow>T\<^sub>2" using algorithmic_path_type_unicity by simp
   then have "T\<^sub>1' = T\<^sub>1" by (simp add: ty.inject) 
   then have "\<Gamma> \<turnstile> s \<Leftrightarrow> v : T\<^sub>1" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^sub>1\<rightarrow>T\<^sub>2" using ih1 ih2 ha hb by auto
   then show "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^sub>2" using eq by auto
 qed (auto)
 
 lemma algorithmic_weak_head_closure:
   shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> s' \<leadsto> s \<Longrightarrow> t' \<leadsto> t \<Longrightarrow> \<Gamma> \<turnstile> s' \<Leftrightarrow> t' : T"
-apply (nominal_induct \<Gamma> s t T avoiding: s' t'  
-    rule: alg_equiv_alg_path_equiv.strong_inducts(1) [of _ _ _ _ "%a b c d e. True"])
-apply(auto intro!: QAT_Arrow)
-done
+proof (nominal_induct \<Gamma> s t T avoiding: s' t'  
+    rule: alg_equiv_alg_path_equiv.strong_inducts(1) [of _ _ _ _ "\<lambda>a b c d e. True"])
+qed(auto intro!: QAT_Arrow)
 
 lemma algorithmic_monotonicity:
   shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T"
   and   "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<subseteq> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T"
 proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv.strong_inducts)
  case (QAT_Arrow x \<Gamma> s t T\<^sub>1 T\<^sub>2 \<Gamma>')
   have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>\<Gamma>'" by fact+
   have h2:"\<Gamma> \<subseteq> \<Gamma>'" by fact
   have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T\<^sub>1)#\<Gamma> \<subseteq> \<Gamma>'; valid \<Gamma>'\<rbrakk>  \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^sub>2" by fact
   have "valid \<Gamma>'" by fact
   then have "valid ((x,T\<^sub>1)#\<Gamma>')" using fs by auto
   moreover
   have sub: "(x,T\<^sub>1)#\<Gamma> \<subseteq> (x,T\<^sub>1)#\<Gamma>'" using h2 by auto
   ultimately have "(x,T\<^sub>1)#\<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^sub>2" using ih by simp
-  then show "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^sub>1\<rightarrow>T\<^sub>2" using fs by (auto simp add: fresh_prod)
+  then show "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^sub>1\<rightarrow>T\<^sub>2" using fs by (auto simp: fresh_prod)
 qed (auto)
 
 lemma path_equiv_implies_nf:
   assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
   shows "s \<leadsto>|" and "t \<leadsto>|"
 using assms
 by (induct rule: alg_equiv_alg_path_equiv.inducts(2)) (simp, auto)
 
 section \<open>Logical Equivalence\<close>
 
 function log_equiv :: "(Ctxt \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool)" ("_ \<turnstile> _ is _ : _" [60,60,60,60] 60) 
 where    
    "\<Gamma> \<turnstile> s is t : TUnit = True"
  | "\<Gamma> \<turnstile> s is t : TBase = \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase"
  | "\<Gamma> \<turnstile> s is t : (T\<^sub>1 \<rightarrow> T\<^sub>2) =  
     (\<forall>\<Gamma>' s' t'. \<Gamma>\<subseteq>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^sub>1 \<longrightarrow>  (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^sub>2))"
-apply (auto simp add: ty.inject)
-apply (subgoal_tac "(\<exists>T\<^sub>1 T\<^sub>2. b=T\<^sub>1 \<rightarrow> T\<^sub>2) \<or> b=TUnit \<or> b=TBase" )
-apply (force)
-apply (rule ty_cases)
-done
+using ty_cases by (force simp: ty.inject)+
 
 termination by lexicographic_order
 
 lemma logical_monotonicity:
  fixes \<Gamma> \<Gamma>' :: Ctxt
  assumes a1: "\<Gamma> \<turnstile> s is t : T" 
  and     a2: "\<Gamma> \<subseteq> \<Gamma>'" 
  and     a3: "valid \<Gamma>'"
  shows "\<Gamma>' \<turnstile> s is t : T"
 using a1 a2 a3
 proof (induct arbitrary: \<Gamma>' rule: log_equiv.induct)
   case (2 \<Gamma> s t \<Gamma>')
   then show "\<Gamma>' \<turnstile> s is t : TBase" using algorithmic_monotonicity by auto
 next
   case (3 \<Gamma> s t T\<^sub>1 T\<^sub>2 \<Gamma>')
   have "\<Gamma> \<turnstile> s is t : T\<^sub>1\<rightarrow>T\<^sub>2" 
   and  "\<Gamma> \<subseteq> \<Gamma>'" 
   and  "valid \<Gamma>'" by fact+
   then show "\<Gamma>' \<turnstile> s is t : T\<^sub>1\<rightarrow>T\<^sub>2" by simp
 qed (auto)
 
 lemma main_lemma:
   shows "\<Gamma> \<turnstile> s is t : T \<Longrightarrow> valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T" 
     and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> \<Gamma> \<turnstile> p is q : T"
 proof (nominal_induct T arbitrary: \<Gamma> s t p q rule: ty.strong_induct)
   case (Arrow T\<^sub>1 T\<^sub>2)
   { 
     case (1 \<Gamma> s t)
     have ih1:"\<And>\<Gamma> s t. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>2; valid \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>2" by fact
     have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T\<^sub>1 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T\<^sub>1" by fact
     have h:"\<Gamma> \<turnstile> s is t : T\<^sub>1\<rightarrow>T\<^sub>2" by fact
     obtain x::name where fs:"x\<sharp>(\<Gamma>,s,t)" by (erule exists_fresh[OF fs_name1])
     have "valid \<Gamma>" by fact
     then have v: "valid ((x,T\<^sub>1)#\<Gamma>)" using fs by auto
     then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T\<^sub>1" by auto
     then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> Var x is Var x : T\<^sub>1" using ih2 by auto
     then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) is App t (Var x) : T\<^sub>2" using h v by auto
     then have "(x,T\<^sub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^sub>2" using ih1 v by auto
-    then show "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1\<rightarrow>T\<^sub>2" using fs by (auto simp add: fresh_prod)
+    then show "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1\<rightarrow>T\<^sub>2" using fs by (auto simp: fresh_prod)
   next
     case (2 \<Gamma> p q)
     have h: "\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^sub>1\<rightarrow>T\<^sub>2" by fact
     have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T\<^sub>2 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T\<^sub>2" by fact
     have ih2:"\<And>\<Gamma> s t. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>1; valid \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^sub>1" by fact
     {
       fix \<Gamma>' s t
       assume "\<Gamma> \<subseteq> \<Gamma>'" and hl:"\<Gamma>' \<turnstile> s is t : T\<^sub>1" and hk: "valid \<Gamma>'"
       then have "\<Gamma>' \<turnstile> p \<leftrightarrow> q : T\<^sub>1 \<rightarrow> T\<^sub>2" using h algorithmic_monotonicity by auto
       moreover have "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^sub>1" using ih2 hl hk by auto
       ultimately have "\<Gamma>' \<turnstile> App p s \<leftrightarrow> App q t : T\<^sub>2" by auto
       then have "\<Gamma>' \<turnstile> App p s is App q t : T\<^sub>2" using ih1 by auto
     }
     then show "\<Gamma> \<turnstile> p is q : T\<^sub>1\<rightarrow>T\<^sub>2"  by simp
   }
 next
   case TBase
   { case 2
     have h:"\<Gamma> \<turnstile> s \<leftrightarrow> t : TBase" by fact
     then have "s \<leadsto>|" and "t \<leadsto>|" using path_equiv_implies_nf by auto
     then have "s \<Down> s" and "t \<Down> t" by auto
     then have "\<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase" using h by auto
     then show "\<Gamma> \<turnstile> s is t : TBase" by auto
   }
 qed (auto elim: alg_path_equiv_implies_valid) 
 
 corollary corollary_main:
   assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
   shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T"
 using a main_lemma alg_path_equiv_implies_valid by blast
 
 lemma logical_symmetry:
   assumes a: "\<Gamma> \<turnstile> s is t : T"
   shows "\<Gamma> \<turnstile> t is s : T"
 using a 
 by (nominal_induct arbitrary: \<Gamma> s t rule: ty.strong_induct) 
-   (auto simp add: algorithmic_symmetry)
+   (auto simp: algorithmic_symmetry)
 
 lemma logical_transitivity:
   assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma> \<turnstile> t is u : T" 
   shows "\<Gamma> \<turnstile> s is u : T"
 using assms
 proof (nominal_induct arbitrary: \<Gamma> s t u  rule:ty.strong_induct)
   case TBase
   then show "\<Gamma> \<turnstile> s is u : TBase" by (auto elim:  algorithmic_transitivity)
 next 
   case (Arrow T\<^sub>1 T\<^sub>2 \<Gamma> s t u)
   have h1:"\<Gamma> \<turnstile> s is t : T\<^sub>1 \<rightarrow> T\<^sub>2" by fact
   have h2:"\<Gamma> \<turnstile> t is u : T\<^sub>1 \<rightarrow> T\<^sub>2" by fact
   have ih1:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>1; \<Gamma> \<turnstile> t is u : T\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^sub>1" by fact
   have ih2:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>2; \<Gamma> \<turnstile> t is u : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^sub>2" by fact
   {
     fix \<Gamma>' s' u'
     assume hsub:"\<Gamma> \<subseteq> \<Gamma>'" and hl:"\<Gamma>' \<turnstile> s' is u' : T\<^sub>1" and hk: "valid \<Gamma>'"
     then have "\<Gamma>' \<turnstile> u' is s' : T\<^sub>1" using logical_symmetry by blast
     then have "\<Gamma>' \<turnstile> u' is u' : T\<^sub>1" using ih1 hl by blast
     then have "\<Gamma>' \<turnstile> App t u' is App u u' : T\<^sub>2" using h2 hsub hk by auto
     moreover have "\<Gamma>' \<turnstile>  App s s' is App t u' : T\<^sub>2" using h1 hsub hl hk by auto
     ultimately have "\<Gamma>' \<turnstile>  App s s' is App u u' : T\<^sub>2" using ih2 by blast
   }
   then show "\<Gamma> \<turnstile> s is u : T\<^sub>1 \<rightarrow> T\<^sub>2" by auto
 qed (auto)
 
 lemma logical_weak_head_closure:
   assumes a: "\<Gamma> \<turnstile> s is t : T" 
   and     b: "s' \<leadsto> s" 
   and     c: "t' \<leadsto> t"
   shows "\<Gamma> \<turnstile> s' is t' : T"
 using a b c algorithmic_weak_head_closure 
-by (nominal_induct arbitrary: \<Gamma> s t s' t' rule: ty.strong_induct) 
-   (auto, blast)
+proof (nominal_induct arbitrary: \<Gamma> s t s' t' rule: ty.strong_induct)
+next
+  case (Arrow ty1 ty2)
+  then show ?case
+    by (smt (verit, ccfv_threshold) QAR_App log_equiv.simps(3))
+qed auto
+   
 
 lemma logical_weak_head_closure':
   assumes "\<Gamma> \<turnstile> s is t : T" and "s' \<leadsto> s" 
   shows "\<Gamma> \<turnstile> s' is t : T"
 using assms
 proof (nominal_induct arbitrary: \<Gamma> s t s' rule: ty.strong_induct)
   case (TBase  \<Gamma> s t s')
   then show ?case by force
 next
   case (TUnit \<Gamma> s t s')
   then show ?case by auto
 next 
   case (Arrow T\<^sub>1 T\<^sub>2 \<Gamma> s t s')
   have h1:"s' \<leadsto> s" by fact
   have ih:"\<And>\<Gamma> s t s'. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^sub>2; s' \<leadsto> s\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' is t : T\<^sub>2" by fact
   have h2:"\<Gamma> \<turnstile> s is t : T\<^sub>1\<rightarrow>T\<^sub>2" by fact
   then 
   have hb:"\<forall>\<Gamma>' s' t'. \<Gamma>\<subseteq>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^sub>1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^sub>2)" 
     by auto
   {
     fix \<Gamma>' s\<^sub>2 t\<^sub>2
     assume "\<Gamma> \<subseteq> \<Gamma>'" and "\<Gamma>' \<turnstile> s\<^sub>2 is t\<^sub>2 : T\<^sub>1" and "valid \<Gamma>'"
     then have "\<Gamma>' \<turnstile> (App s s\<^sub>2) is (App t t\<^sub>2) : T\<^sub>2" using hb by auto
     moreover have "(App s' s\<^sub>2)  \<leadsto> (App s s\<^sub>2)" using h1 by auto  
     ultimately have "\<Gamma>' \<turnstile> App s' s\<^sub>2 is App t t\<^sub>2 : T\<^sub>2" using ih by auto
   }
   then show "\<Gamma> \<turnstile> s' is t : T\<^sub>1\<rightarrow>T\<^sub>2" by auto
 qed 
 
 abbreviation 
  log_equiv_for_psubsts :: "Ctxt \<Rightarrow> Subst \<Rightarrow> Subst \<Rightarrow> Ctxt \<Rightarrow> bool"  ("_ \<turnstile> _ is _ over _" [60,60] 60) 
 where
   "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma> \<equiv> \<forall>x T. (x,T) \<in> set \<Gamma> \<longrightarrow> \<Gamma>' \<turnstile> \<theta><Var x> is  \<theta>'<Var x> : T"
 
 lemma logical_pseudo_reflexivity:
   assumes "\<Gamma>' \<turnstile> t is s over \<Gamma>"
-  shows "\<Gamma>' \<turnstile> s is s over \<Gamma>" 
-proof -
-  from assms have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast
-  with assms show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast
-qed
+  shows "\<Gamma>' \<turnstile> s is s over \<Gamma>"
+  by (meson assms logical_symmetry logical_transitivity) 
 
 lemma logical_subst_monotonicity :
   fixes \<Gamma> \<Gamma>' \<Gamma>'' :: Ctxt
   assumes a: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   and     b: "\<Gamma>' \<subseteq> \<Gamma>''"
   and     c: "valid \<Gamma>''"
   shows "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
 using a b c logical_monotonicity by blast
 
 lemma equiv_subst_ext :
   assumes h1: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   and     h2: "\<Gamma>' \<turnstile> s is t : T" 
   and     fs: "x\<sharp>\<Gamma>"
   shows "\<Gamma>' \<turnstile> (x,s)#\<theta> is (x,t)#\<theta>' over (x,T)#\<Gamma>"
 using assms
 proof -
   {
     fix y U
     assume "(y,U) \<in> set ((x,T)#\<Gamma>)"
     moreover
     { 
       assume "(y,U) \<in> set [(x,T)]"
       with h2 have "\<Gamma>' \<turnstile> ((x,s)#\<theta>)<Var y> is ((x,t)#\<theta>')<Var y> : U" by auto 
     }
     moreover
     {
       assume hl:"(y,U) \<in> set \<Gamma>"
-      then have "\<not> y\<sharp>\<Gamma>" by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_atm fresh_prod)
-      then have hf:"x\<sharp> Var y" using fs by (auto simp add: fresh_atm)
+      then have "\<not> y\<sharp>\<Gamma>" by (induct \<Gamma>) (auto simp: fresh_list_cons fresh_atm fresh_prod)
+      then have hf:"x\<sharp> Var y" using fs by (auto simp: fresh_atm)
       then have "((x,s)#\<theta>)<Var y> = \<theta><Var y>" "((x,t)#\<theta>')<Var y> = \<theta>'<Var y>" 
         using fresh_psubst_simp by blast+ 
       moreover have  "\<Gamma>' \<turnstile> \<theta><Var y> is \<theta>'<Var y> : U" using h1 hl by auto
       ultimately have "\<Gamma>' \<turnstile> ((x,s)#\<theta>)<Var y> is ((x,t)#\<theta>')<Var y> : U" by auto
     }
     ultimately have "\<Gamma>' \<turnstile> ((x,s)#\<theta>)<Var y> is ((x,t)#\<theta>')<Var y> : U" by auto
   }
   then show "\<Gamma>' \<turnstile> (x,s)#\<theta> is (x,t)#\<theta>' over (x,T)#\<Gamma>" by auto
 qed
 
 theorem fundamental_theorem_1:
   assumes a1: "\<Gamma> \<turnstile> t : T" 
   and     a2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
   and     a3: "valid \<Gamma>'" 
   shows "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T"   
 using a1 a2 a3
 proof (nominal_induct \<Gamma> t T avoiding: \<theta> \<theta>' arbitrary: \<Gamma>' rule: typing.strong_induct)
   case (T_Lam x \<Gamma> T\<^sub>1 t\<^sub>2 T\<^sub>2 \<theta> \<theta>' \<Gamma>')
   have vc: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" "x\<sharp>\<Gamma>" by fact+
   have asm1: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact
   have ih:"\<And>\<theta> \<theta>' \<Gamma>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^sub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t\<^sub>2> is \<theta>'<t\<^sub>2> : T\<^sub>2" by fact
   show "\<Gamma>' \<turnstile> \<theta><Lam [x].t\<^sub>2> is \<theta>'<Lam [x].t\<^sub>2> : T\<^sub>1\<rightarrow>T\<^sub>2" using vc
   proof (simp, intro strip)
     fix \<Gamma>'' s' t'
     assume sub: "\<Gamma>' \<subseteq> \<Gamma>''" 
     and    asm2: "\<Gamma>''\<turnstile> s' is t' : T\<^sub>1" 
     and    val: "valid \<Gamma>''"
     from asm1 val sub have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using logical_subst_monotonicity by blast
     with asm2 vc have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^sub>1)#\<Gamma>" using equiv_subst_ext by blast
     with ih val have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<t\<^sub>2> is ((x,t')#\<theta>')<t\<^sub>2> : T\<^sub>2" by auto
     with vc have "\<Gamma>''\<turnstile>\<theta><t\<^sub>2>[x::=s'] is \<theta>'<t\<^sub>2>[x::=t'] : T\<^sub>2" by (simp add: psubst_subst_psubst)
     moreover 
     have "App (Lam [x].\<theta><t\<^sub>2>) s' \<leadsto> \<theta><t\<^sub>2>[x::=s']" by auto
     moreover 
     have "App (Lam [x].\<theta>'<t\<^sub>2>) t' \<leadsto> \<theta>'<t\<^sub>2>[x::=t']" by auto
     ultimately show "\<Gamma>''\<turnstile> App (Lam [x].\<theta><t\<^sub>2>) s' is App (Lam [x].\<theta>'<t\<^sub>2>) t' : T\<^sub>2" 
       using logical_weak_head_closure by auto
   qed
 qed (auto)
 
 
 theorem fundamental_theorem_2:
   assumes h1: "\<Gamma> \<turnstile> s \<equiv> t : T" 
   and     h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
   and     h3: "valid \<Gamma>'"
   shows "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T"
 using h1 h2 h3
 proof (nominal_induct \<Gamma> s t T avoiding: \<Gamma>' \<theta> \<theta>' rule: def_equiv.strong_induct)
   case (Q_Refl \<Gamma> t T \<Gamma>' \<theta> \<theta>')
-  have "\<Gamma> \<turnstile> t : T" 
-  and  "valid \<Gamma>'" by fact+
-  moreover 
-  have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" by fact
-  ultimately show "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T" using fundamental_theorem_1 by blast
+  then show "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T" using fundamental_theorem_1
+    by blast
 next
   case (Q_Symm \<Gamma> t s T \<Gamma>' \<theta> \<theta>')
-  have "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
-  and "valid \<Gamma>'" by fact+
-  moreover 
-  have ih: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<s> : T" by fact
-  ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using logical_symmetry by blast
+  then show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using logical_symmetry by blast
 next
   case (Q_Trans \<Gamma> s t T u \<Gamma>' \<theta> \<theta>')
   have ih1: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" by fact
   have ih2: "\<And> \<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t> is \<theta>'<u> : T" by fact
   have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   and  v: "valid \<Gamma>'" by fact+
   then have "\<Gamma>' \<turnstile> \<theta>' is \<theta>' over \<Gamma>" using logical_pseudo_reflexivity by auto
   then have "\<Gamma>' \<turnstile> \<theta>'<t> is \<theta>'<u> : T" using ih2 v by auto
   moreover have "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T" using ih1 h v by auto
   ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<u> : T" using logical_transitivity by blast
 next
   case (Q_Abs x \<Gamma> T\<^sub>1 s\<^sub>2 t\<^sub>2 T\<^sub>2 \<Gamma>' \<theta> \<theta>')
   have fs:"x\<sharp>\<Gamma>" by fact
   have fs2: "x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+
   have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   and  h3: "valid \<Gamma>'" by fact+
   have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^sub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^sub>2> is \<theta>'<t\<^sub>2> : T\<^sub>2" by fact
   {
     fix \<Gamma>'' s' t'
     assume "\<Gamma>' \<subseteq> \<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^sub>1" and hk: "valid \<Gamma>''"
     then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using h2 logical_subst_monotonicity by blast
     then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^sub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
     then have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<s\<^sub>2> is ((x,t')#\<theta>')<t\<^sub>2> : T\<^sub>2" using ih hk by blast
     then have "\<Gamma>''\<turnstile> \<theta><s\<^sub>2>[x::=s'] is \<theta>'<t\<^sub>2>[x::=t'] : T\<^sub>2" using fs2 psubst_subst_psubst by auto
     moreover have "App (Lam [x]. \<theta><s\<^sub>2>) s' \<leadsto>  \<theta><s\<^sub>2>[x::=s']" 
               and "App (Lam [x].\<theta>'<t\<^sub>2>) t' \<leadsto> \<theta>'<t\<^sub>2>[x::=t']" by auto
     ultimately have "\<Gamma>'' \<turnstile> App (Lam [x]. \<theta><s\<^sub>2>) s' is App (Lam [x].\<theta>'<t\<^sub>2>) t' : T\<^sub>2" 
       using logical_weak_head_closure by auto
   }
   moreover have "valid \<Gamma>'" by fact
   ultimately have "\<Gamma>' \<turnstile> Lam [x].\<theta><s\<^sub>2> is Lam [x].\<theta>'<t\<^sub>2> : T\<^sub>1\<rightarrow>T\<^sub>2" by auto
   then show "\<Gamma>' \<turnstile> \<theta><Lam [x].s\<^sub>2> is \<theta>'<Lam [x].t\<^sub>2> : T\<^sub>1\<rightarrow>T\<^sub>2" using fs2 by auto
 next
   case (Q_App \<Gamma> s\<^sub>1 t\<^sub>1 T\<^sub>1 T\<^sub>2 s\<^sub>2 t\<^sub>2 \<Gamma>' \<theta> \<theta>')
   then show "\<Gamma>' \<turnstile> \<theta><App s\<^sub>1 s\<^sub>2> is \<theta>'<App t\<^sub>1 t\<^sub>2> : T\<^sub>2" by auto 
 next
   case (Q_Beta x \<Gamma> s\<^sub>2 t\<^sub>2 T\<^sub>1 s12 t12 T\<^sub>2 \<Gamma>' \<theta> \<theta>')
   have h: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   and  h': "valid \<Gamma>'" by fact+
   have fs: "x\<sharp>\<Gamma>" by fact
   have fs2: " x\<sharp>\<theta>" "x\<sharp>\<theta>'" by fact+
   have ih1: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^sub>2> is \<theta>'<t\<^sub>2> : T\<^sub>1" by fact
   have ih2: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^sub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s12> is \<theta>'<t12> : T\<^sub>2" by fact
   have "\<Gamma>' \<turnstile> \<theta><s\<^sub>2> is \<theta>'<t\<^sub>2> : T\<^sub>1" using ih1 h' h by auto
   then have "\<Gamma>' \<turnstile> (x,\<theta><s\<^sub>2>)#\<theta> is (x,\<theta>'<t\<^sub>2>)#\<theta>' over (x,T\<^sub>1)#\<Gamma>" using equiv_subst_ext h fs by blast
   then have "\<Gamma>' \<turnstile> ((x,\<theta><s\<^sub>2>)#\<theta>)<s12> is ((x,\<theta>'<t\<^sub>2>)#\<theta>')<t12> : T\<^sub>2" using ih2 h' by auto
   then have "\<Gamma>' \<turnstile> \<theta><s12>[x::=\<theta><s\<^sub>2>] is \<theta>'<t12>[x::=\<theta>'<t\<^sub>2>] : T\<^sub>2" using fs2 psubst_subst_psubst by auto
   then have "\<Gamma>' \<turnstile> \<theta><s12>[x::=\<theta><s\<^sub>2>] is \<theta>'<t12[x::=t\<^sub>2]> : T\<^sub>2" using fs2 psubst_subst_propagate by auto
   moreover have "App (Lam [x].\<theta><s12>) (\<theta><s\<^sub>2>) \<leadsto> \<theta><s12>[x::=\<theta><s\<^sub>2>]" by auto 
   ultimately have "\<Gamma>' \<turnstile> App (Lam [x].\<theta><s12>) (\<theta><s\<^sub>2>) is \<theta>'<t12[x::=t\<^sub>2]> : T\<^sub>2" 
     using logical_weak_head_closure' by auto
   then show "\<Gamma>' \<turnstile> \<theta><App (Lam [x].s12) s\<^sub>2> is \<theta>'<t12[x::=t\<^sub>2]> : T\<^sub>2" using fs2 by simp
 next
   case (Q_Ext x \<Gamma> s t T\<^sub>1 T\<^sub>2 \<Gamma>' \<theta> \<theta>')
   have h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>" 
   and  h2': "valid \<Gamma>'" by fact+
   have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact+
   have ih:"\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^sub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> 
                           \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><App s (Var x)> is \<theta>'<App t (Var x)> : T\<^sub>2" by fact
    {
     fix \<Gamma>'' s' t'
     assume hsub: "\<Gamma>' \<subseteq> \<Gamma>''" and hl: "\<Gamma>''\<turnstile> s' is t' : T\<^sub>1" and hk: "valid \<Gamma>''"
     then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using h2 logical_subst_monotonicity by blast
     then have "\<Gamma>'' \<turnstile> (x,s')#\<theta> is (x,t')#\<theta>' over (x,T\<^sub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
     then have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<App s (Var x)>  is ((x,t')#\<theta>')<App t (Var x)> : T\<^sub>2" using ih hk by blast
     then 
     have "\<Gamma>'' \<turnstile> App (((x,s')#\<theta>)<s>) (((x,s')#\<theta>)<(Var x)>) is App (((x,t')#\<theta>')<t>) (((x,t')#\<theta>')<(Var x)>) : T\<^sub>2"
       by auto
     then have "\<Gamma>'' \<turnstile> App ((x,s')#\<theta>)<s> s'  is App ((x,t')#\<theta>')<t> t' : T\<^sub>2" by auto
     then have "\<Gamma>'' \<turnstile> App (\<theta><s>) s' is App (\<theta>'<t>) t' : T\<^sub>2" using fs fresh_psubst_simp by auto
   }
   moreover have "valid \<Gamma>'" by fact
   ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T\<^sub>1\<rightarrow>T\<^sub>2" by auto
 next
   case (Q_Unit \<Gamma> s t \<Gamma>' \<theta> \<theta>')  
   then show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : TUnit" by auto
 qed
 
 
 theorem completeness:
   assumes asm: "\<Gamma> \<turnstile> s \<equiv> t : T"
   shows   "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T"
 proof -
   have val: "valid \<Gamma>" using def_equiv_implies_valid asm by simp
-  moreover
-  {
-    fix x T
-    assume "(x,T) \<in> set \<Gamma>" "valid \<Gamma>"
-    then have "\<Gamma> \<turnstile> Var x is Var x : T" using main_lemma(2) by blast
-  }
-  ultimately have "\<Gamma> \<turnstile> [] is [] over \<Gamma>" by auto 
+  then have "\<Gamma> \<turnstile> [] is [] over \<Gamma>"
+    by (simp add: QAP_Var main_lemma(2)) 
   then have "\<Gamma> \<turnstile> []<s> is []<t> : T" using fundamental_theorem_2 val asm by blast
   then have "\<Gamma> \<turnstile> s is t : T" by simp
   then show  "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" using main_lemma(1) val by simp
 qed
 
 text \<open>We leave soundness as an exercise - just like Crary in the ATS book :-) \\ 
  @{prop[mode=IfThen] "\<lbrakk>\<Gamma> \<turnstile> s \<Leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T"} \\
  \<^prop>\<open>\<lbrakk>\<Gamma> \<turnstile> s \<leftrightarrow> t : T; \<Gamma> \<turnstile> t : T; \<Gamma> \<turnstile> s : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T\<close> 
 \<close>
 
 end
 
diff --git a/src/HOL/Nominal/Examples/Fsub.thy b/src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy
+++ b/src/HOL/Nominal/Examples/Fsub.thy
@@ -1,1853 +1,1849 @@
 (*<*)
 theory Fsub
 imports "HOL-Nominal.Nominal" 
 begin
 (*>*)
 
 text\<open>Authors: Christian Urban,
                 Benjamin Pierce,
                 Dimitrios Vytiniotis
                 Stephanie Weirich
                 Steve Zdancewic
                 Julien Narboux
                 Stefan Berghofer
 
        with great help from Markus Wenzel.\<close>
 
 section \<open>Types for Names, Nominal Datatype Declaration for Types and Terms\<close>
 
 no_syntax
   "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  ("(1[_])")
 
 text \<open>The main point of this solution is to use names everywhere (be they bound, 
   binding or free). In System \FSUB{} there are two kinds of names corresponding to 
   type-variables and to term-variables. These two kinds of names are represented in 
   the nominal datatype package as atom-types \<open>tyvrs\<close> and \<open>vrs\<close>:\<close>
 
 atom_decl tyvrs vrs
 
 text\<open>There are numerous facts that come with this declaration: for example that 
   there are infinitely many elements in \<open>tyvrs\<close> and \<open>vrs\<close>.\<close>
 
 text\<open>The constructors for types and terms in System \FSUB{} contain abstractions 
   over type-variables and term-variables. The nominal datatype package uses 
   \<open>\<guillemotleft>\<dots>\<guillemotright>\<dots>\<close> to indicate where abstractions occur.\<close>
 
 nominal_datatype ty = 
     Tvar   "tyvrs"
   | Top
   | Arrow  "ty" "ty"         (infixr "\<rightarrow>" 200)
   | Forall "\<guillemotleft>tyvrs\<guillemotright>ty" "ty" 
 
 nominal_datatype trm = 
     Var   "vrs"
   | Abs   "\<guillemotleft>vrs\<guillemotright>trm" "ty" 
   | TAbs  "\<guillemotleft>tyvrs\<guillemotright>trm" "ty"
   | App   "trm" "trm" (infixl "\<cdot>" 200)
   | TApp  "trm" "ty"  (infixl "\<cdot>\<^sub>\<tau>" 200)
 
 text \<open>To be polite to the eye, some more familiar notation is introduced. 
   Because of the change in the order of arguments, one needs to use 
   translation rules, instead of syntax annotations at the term-constructors
   as given above for \<^term>\<open>Arrow\<close>.\<close>
 
 abbreviation
   Forall_syn :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty"  ("(3\<forall>_<:_./ _)" [0, 0, 10] 10) 
 where
   "\<forall>X<:T\<^sub>1. T\<^sub>2 \<equiv> ty.Forall X T\<^sub>2 T\<^sub>1"
 
 abbreviation
   Abs_syn    :: "vrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm"  ("(3\<lambda>_:_./ _)" [0, 0, 10] 10) 
 where
   "\<lambda>x:T. t \<equiv> trm.Abs x t T"
 
 abbreviation
   TAbs_syn   :: "tyvrs \<Rightarrow> ty \<Rightarrow> trm \<Rightarrow> trm" ("(3\<lambda>_<:_./ _)" [0, 0, 10] 10) 
 where
   "\<lambda>X<:T. t \<equiv> trm.TAbs X t T"
 
 text \<open>Again there are numerous facts that are proved automatically for \<^typ>\<open>ty\<close> 
   and \<^typ>\<open>trm\<close>: for example that the set of free variables, i.e.~the \<open>support\<close>, 
   is finite. However note that nominal-datatype declarations do \emph{not} define 
   ``classical" constructor-based datatypes, but rather define $\alpha$-equivalence 
   classes---we can for example show that $\alpha$-equivalent \<^typ>\<open>ty\<close>s 
   and \<^typ>\<open>trm\<close>s are equal:\<close>
 
 lemma alpha_illustration:
   shows "(\<forall>X<:T. Tvar X) = (\<forall>Y<:T. Tvar Y)"
   and   "(\<lambda>x:T. Var x) = (\<lambda>y:T. Var y)"
   by (simp_all add: ty.inject trm.inject alpha calc_atm fresh_atm)
 
 section \<open>SubTyping Contexts\<close>
 
 nominal_datatype binding = 
     VarB vrs ty 
   | TVarB tyvrs ty
 
 type_synonym env = "binding list"
 
 text \<open>Typing contexts are represented as lists that ``grow" on the left; we
   thereby deviating from the convention in the POPLmark-paper. The lists contain
   pairs of type-variables and types (this is sufficient for Part 1A).\<close>
 
 text \<open>In order to state validity-conditions for typing-contexts, the notion of
   a \<open>dom\<close> of a typing-context is handy.\<close>
 
 nominal_primrec
   "tyvrs_of" :: "binding \<Rightarrow> tyvrs set"
 where
   "tyvrs_of (VarB  x y) = {}"
 | "tyvrs_of (TVarB x y) = {x}"
 by auto
 
 nominal_primrec
   "vrs_of" :: "binding \<Rightarrow> vrs set"
 where
   "vrs_of (VarB  x y) = {x}"
 | "vrs_of (TVarB x y) = {}"
 by auto
 
 primrec
   "ty_dom" :: "env \<Rightarrow> tyvrs set"
 where
   "ty_dom [] = {}"
 | "ty_dom (X#\<Gamma>) = (tyvrs_of X)\<union>(ty_dom \<Gamma>)" 
 
 primrec
   "trm_dom" :: "env \<Rightarrow> vrs set"
 where
   "trm_dom [] = {}"
 | "trm_dom (X#\<Gamma>) = (vrs_of X)\<union>(trm_dom \<Gamma>)" 
 
 lemma vrs_of_eqvt[eqvt]:
   fixes pi ::"tyvrs prm"
   and   pi'::"vrs   prm"
   shows "pi \<bullet>(tyvrs_of x) = tyvrs_of (pi\<bullet>x)"
   and   "pi'\<bullet>(tyvrs_of x) = tyvrs_of (pi'\<bullet>x)"
   and   "pi \<bullet>(vrs_of x)   = vrs_of   (pi\<bullet>x)"
   and   "pi'\<bullet>(vrs_of x)   = vrs_of   (pi'\<bullet>x)"
 by (nominal_induct x rule: binding.strong_induct) (simp_all add: tyvrs_of.simps eqvts)
 
 lemma doms_eqvt[eqvt]:
   fixes pi::"tyvrs prm"
   and   pi'::"vrs prm"
   shows "pi \<bullet>(ty_dom \<Gamma>)  = ty_dom  (pi\<bullet>\<Gamma>)"
   and   "pi'\<bullet>(ty_dom \<Gamma>)  = ty_dom  (pi'\<bullet>\<Gamma>)"
   and   "pi \<bullet>(trm_dom \<Gamma>) = trm_dom (pi\<bullet>\<Gamma>)"
   and   "pi'\<bullet>(trm_dom \<Gamma>) = trm_dom (pi'\<bullet>\<Gamma>)"
 by (induct \<Gamma>) (simp_all add: eqvts)
 
 lemma finite_vrs:
   shows "finite (tyvrs_of x)"
   and   "finite (vrs_of x)"
 by (nominal_induct rule:binding.strong_induct) auto
  
 lemma finite_doms:
   shows "finite (ty_dom \<Gamma>)"
   and   "finite (trm_dom \<Gamma>)"
 by (induct \<Gamma>) (auto simp: finite_vrs)
 
 lemma ty_dom_supp:
   shows "(supp (ty_dom  \<Gamma>)) = (ty_dom  \<Gamma>)"
   and   "(supp (trm_dom \<Gamma>)) = (trm_dom \<Gamma>)"
 by (simp only: at_fin_set_supp at_tyvrs_inst at_vrs_inst finite_doms)+
 
 lemma ty_dom_inclusion:
   assumes a: "(TVarB X T)\<in>set \<Gamma>" 
   shows "X\<in>(ty_dom \<Gamma>)"
 using a by (induct \<Gamma>) (auto)
 
 lemma ty_binding_existence:
   assumes "X \<in> (tyvrs_of a)"
   shows "\<exists>T.(TVarB X T=a)"
   using assms
 by (nominal_induct a rule: binding.strong_induct) (auto)
 
 lemma ty_dom_existence:
   assumes a: "X\<in>(ty_dom \<Gamma>)" 
   shows "\<exists>T.(TVarB X T)\<in>set \<Gamma>"
   using a 
 proof (induction \<Gamma>)
   case Nil then show ?case by simp
 next
   case (Cons a \<Gamma>) then show ?case
     using ty_binding_existence by fastforce
 qed
 
 lemma doms_append:
   shows "ty_dom (\<Gamma>@\<Delta>) = ((ty_dom \<Gamma>) \<union> (ty_dom \<Delta>))"
   and   "trm_dom (\<Gamma>@\<Delta>) = ((trm_dom \<Gamma>) \<union> (trm_dom \<Delta>))"
   by (induct \<Gamma>) (auto)
 
 lemma ty_vrs_prm_simp:
   fixes pi::"vrs prm"
   and   S::"ty"
   shows "pi\<bullet>S = S"
 by (induct S rule: ty.induct) (auto simp: calc_atm)
 
 lemma fresh_ty_dom_cons:
   fixes X::"tyvrs"
   shows "X\<sharp>(ty_dom (Y#\<Gamma>)) = (X\<sharp>(tyvrs_of Y) \<and> X\<sharp>(ty_dom \<Gamma>))"
 proof (nominal_induct rule:binding.strong_induct)
   case (VarB vrs ty)
   then show ?case by auto
 next
   case (TVarB tyvrs ty)
   then show ?case
     by (simp add: at_fin_set_supp at_tyvrs_inst finite_doms(1) fresh_def supp_atm(1))
 qed
 
 lemma tyvrs_fresh:
   fixes   X::"tyvrs"
   assumes "X \<sharp> a" 
   shows   "X \<sharp> tyvrs_of a"
   and     "X \<sharp> vrs_of a"
   using assms
   by (nominal_induct a rule:binding.strong_induct) (force simp: fresh_singleton)+
 
 lemma fresh_dom:
   fixes X::"tyvrs"
   assumes a: "X\<sharp>\<Gamma>" 
   shows "X\<sharp>(ty_dom \<Gamma>)"
 using a
 proof (induct \<Gamma>)
   case Nil then show ?case by auto
 next
   case (Cons a \<Gamma>) then show ?case
     by (meson fresh_list_cons fresh_ty_dom_cons tyvrs_fresh(1))
 qed
 
 text \<open>Not all lists of type \<^typ>\<open>env\<close> are well-formed. One condition
   requires that in \<^term>\<open>TVarB X S#\<Gamma>\<close> all free variables of \<^term>\<open>S\<close> must be 
   in the \<^term>\<open>ty_dom\<close> of \<^term>\<open>\<Gamma>\<close>, that is \<^term>\<open>S\<close> must be \<open>closed\<close> 
   in \<^term>\<open>\<Gamma>\<close>. The set of free variables of \<^term>\<open>S\<close> is the 
   \<open>support\<close> of \<^term>\<open>S\<close>.\<close>
 
 definition "closed_in" :: "ty \<Rightarrow> env \<Rightarrow> bool" ("_ closed'_in _" [100,100] 100) where
   "S closed_in \<Gamma> \<equiv> (supp S)\<subseteq>(ty_dom \<Gamma>)"
 
 lemma closed_in_eqvt[eqvt]:
   fixes pi::"tyvrs prm"
   assumes a: "S closed_in \<Gamma>" 
   shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)"
   using a
 proof -
   from a have "pi\<bullet>(S closed_in \<Gamma>)" by (simp add: perm_bool)
   then show "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)" by (simp add: closed_in_def eqvts)
 qed
 
 lemma tyvrs_vrs_prm_simp:
   fixes pi::"vrs prm"
   shows "tyvrs_of (pi\<bullet>a) = tyvrs_of a"
   by (nominal_induct rule:binding.strong_induct) (auto simp: vrs_prm_tyvrs_def)
 
 lemma ty_vrs_fresh:
   fixes x::"vrs"
   and   T::"ty"
   shows "x \<sharp> T"
 by (simp add: fresh_def supp_def ty_vrs_prm_simp)
 
 lemma ty_dom_vrs_prm_simp:
   fixes pi::"vrs prm"
   and   \<Gamma>::"env"
   shows "(ty_dom (pi\<bullet>\<Gamma>)) = (ty_dom \<Gamma>)"
 by (induct \<Gamma>) (auto simp: tyvrs_vrs_prm_simp)
 
 lemma closed_in_eqvt'[eqvt]:
   fixes pi::"vrs prm"
   assumes a: "S closed_in \<Gamma>" 
   shows "(pi\<bullet>S) closed_in (pi\<bullet>\<Gamma>)"
   using assms closed_in_def ty_dom_vrs_prm_simp ty_vrs_prm_simp by force
 
 lemma fresh_vrs_of: 
   fixes x::"vrs"
   shows "x\<sharp>vrs_of b = x\<sharp>b"
   by (nominal_induct b rule: binding.strong_induct)
     (simp_all add: fresh_singleton fresh_set_empty ty_vrs_fresh fresh_atm)
 
 lemma fresh_trm_dom: 
   fixes x::"vrs"
   shows "x\<sharp> trm_dom \<Gamma> = x\<sharp>\<Gamma>"
   by (induct \<Gamma>)
     (simp_all add: fresh_list_cons
      fresh_fin_union [OF pt_vrs_inst at_vrs_inst fs_vrs_inst]
      finite_doms finite_vrs fresh_vrs_of)
 
 lemma closed_in_fresh: "(X::tyvrs) \<sharp> ty_dom \<Gamma> \<Longrightarrow> T closed_in \<Gamma> \<Longrightarrow> X \<sharp> T"
   by (auto simp: closed_in_def fresh_def ty_dom_supp)
 
 text \<open>Now validity of a context is a straightforward inductive definition.\<close>
   
 inductive
   valid_rel :: "env \<Rightarrow> bool" ("\<turnstile> _ ok" [100] 100)
 where
   valid_nil[simp]:   "\<turnstile> [] ok"
 | valid_consT[simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; X\<sharp>(ty_dom  \<Gamma>); T closed_in \<Gamma>\<rbrakk>  \<Longrightarrow>  \<turnstile> (TVarB X T#\<Gamma>) ok"
 | valid_cons [simp]: "\<lbrakk>\<turnstile> \<Gamma> ok; x\<sharp>(trm_dom \<Gamma>); T closed_in \<Gamma>\<rbrakk>  \<Longrightarrow>  \<turnstile> (VarB  x T#\<Gamma>) ok"
 
 equivariance valid_rel
 
 declare binding.inject [simp add]
 declare trm.inject     [simp add]
 
 inductive_cases validE[elim]: 
   "\<turnstile> (TVarB X T#\<Gamma>) ok" 
   "\<turnstile> (VarB  x T#\<Gamma>) ok" 
   "\<turnstile> (b#\<Gamma>) ok" 
 
 declare binding.inject [simp del]
 declare trm.inject     [simp del]
 
 lemma validE_append:
   assumes a: "\<turnstile> (\<Delta>@\<Gamma>) ok" 
   shows "\<turnstile> \<Gamma> ok"
   using a 
 proof (induct \<Delta>)
   case (Cons a \<Gamma>')
   then show ?case 
     by (nominal_induct a rule:binding.strong_induct) auto
 qed (auto)
 
 lemma replace_type:
   assumes a: "\<turnstile> (\<Delta>@(TVarB X T)#\<Gamma>) ok"
   and     b: "S closed_in \<Gamma>"
   shows "\<turnstile> (\<Delta>@(TVarB X S)#\<Gamma>) ok"
 using a b
 proof(induct \<Delta>)
   case Nil
   then show ?case by (auto intro: valid_cons simp add: doms_append closed_in_def)
 next
   case (Cons a \<Gamma>')
   then show ?case 
     by (nominal_induct a rule:binding.strong_induct)
        (auto intro!: valid_cons simp add: doms_append closed_in_def)
 qed
 
 text \<open>Well-formed contexts have a unique type-binding for a type-variable.\<close> 
 
 lemma uniqueness_of_ctxt:
   fixes \<Gamma>::"env"
   assumes a: "\<turnstile> \<Gamma> ok"
   and     b: "(TVarB X T)\<in>set \<Gamma>"
   and     c: "(TVarB X S)\<in>set \<Gamma>"
   shows "T=S"
 using a b c
 proof (induct)
   case (valid_consT \<Gamma> X' T')
   moreover
   { fix \<Gamma>'::"env"
     assume a: "X'\<sharp>(ty_dom \<Gamma>')" 
     have "\<not>(\<exists>T.(TVarB X' T)\<in>(set \<Gamma>'))" using a 
     proof (induct \<Gamma>')
       case (Cons Y \<Gamma>')
       thus "\<not> (\<exists>T.(TVarB X' T)\<in>set(Y#\<Gamma>'))"
         by (simp add:  fresh_ty_dom_cons 
                        fresh_fin_union[OF pt_tyvrs_inst  at_tyvrs_inst fs_tyvrs_inst]  
                        finite_vrs finite_doms, 
             auto simp: fresh_atm fresh_singleton)
     qed (simp)
   }
   ultimately show "T=S" by (auto simp: binding.inject)
 qed (auto)
 
 lemma uniqueness_of_ctxt':
   fixes \<Gamma>::"env"
   assumes a: "\<turnstile> \<Gamma> ok"
   and     b: "(VarB x T)\<in>set \<Gamma>"
   and     c: "(VarB x S)\<in>set \<Gamma>"
   shows "T=S"
 using a b c
 proof (induct)
   case (valid_cons \<Gamma> x' T')
   moreover
   { fix \<Gamma>'::"env"
     assume a: "x'\<sharp>(trm_dom \<Gamma>')" 
     have "\<not>(\<exists>T.(VarB x' T)\<in>(set \<Gamma>'))" using a 
     proof (induct \<Gamma>')
       case (Cons y \<Gamma>')
       thus "\<not> (\<exists>T.(VarB x' T)\<in>set(y#\<Gamma>'))" 
         by (simp add:  fresh_fin_union[OF pt_vrs_inst  at_vrs_inst fs_vrs_inst]  
                        finite_vrs finite_doms, 
             auto simp: fresh_atm fresh_singleton)
     qed (simp)
   }
   ultimately show "T=S" by (auto simp: binding.inject)
 qed (auto)
 
 section \<open>Size and Capture-Avoiding Substitution for Types\<close>
 
 nominal_primrec
   size_ty :: "ty \<Rightarrow> nat"
 where
   "size_ty (Tvar X) = 1"
 | "size_ty (Top) = 1"
 | "size_ty (T1 \<rightarrow> T2) = (size_ty T1) + (size_ty T2) + 1"
 | "X \<sharp> T1 \<Longrightarrow> size_ty (\<forall>X<:T1. T2) = (size_ty T1) + (size_ty T2) + 1"
   by (finite_guess | fresh_guess | simp)+
 
 nominal_primrec
   subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_ \<mapsto> _]\<^sub>\<tau>" [300, 0, 0] 300)
 where
   "(Tvar X)[Y \<mapsto> T]\<^sub>\<tau> = (if X=Y then T else Tvar X)"
 | "(Top)[Y \<mapsto> T]\<^sub>\<tau> = Top"
 | "(T\<^sub>1 \<rightarrow> T\<^sub>2)[Y \<mapsto> T]\<^sub>\<tau> = T\<^sub>1[Y \<mapsto> T]\<^sub>\<tau> \<rightarrow> T\<^sub>2[Y \<mapsto> T]\<^sub>\<tau>"
 | "X\<sharp>(Y,T,T\<^sub>1) \<Longrightarrow> (\<forall>X<:T\<^sub>1. T\<^sub>2)[Y \<mapsto> T]\<^sub>\<tau> = (\<forall>X<:T\<^sub>1[Y \<mapsto> T]\<^sub>\<tau>. T\<^sub>2[Y \<mapsto> T]\<^sub>\<tau>)"
   by (finite_guess | fresh_guess | simp add: abs_fresh)+
 
 lemma subst_eqvt[eqvt]:
   fixes pi::"tyvrs prm" 
   and   T::"ty"
   shows "pi\<bullet>(T[X \<mapsto> T']\<^sub>\<tau>) = (pi\<bullet>T)[(pi\<bullet>X) \<mapsto> (pi\<bullet>T')]\<^sub>\<tau>"
   by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
      (perm_simp add: fresh_bij)+
 
 lemma subst_eqvt'[eqvt]:
   fixes pi::"vrs prm" 
   and   T::"ty"
   shows "pi\<bullet>(T[X \<mapsto> T']\<^sub>\<tau>) = (pi\<bullet>T)[(pi\<bullet>X) \<mapsto> (pi\<bullet>T')]\<^sub>\<tau>"
   by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
      (perm_simp add: fresh_left)+
 
 lemma type_subst_fresh:
   fixes X::"tyvrs"
   assumes "X\<sharp>T" and "X\<sharp>P"
   shows   "X\<sharp>T[Y \<mapsto> P]\<^sub>\<tau>"
   using assms
   by (nominal_induct T avoiding: X Y P rule:ty.strong_induct)
     (auto simp: abs_fresh)
 
 lemma fresh_type_subst_fresh:
   assumes "X\<sharp>T'"
   shows "X\<sharp>T[X \<mapsto> T']\<^sub>\<tau>"
   using assms 
   by (nominal_induct T avoiding: X T' rule: ty.strong_induct)
      (auto simp: fresh_atm abs_fresh) 
 
 lemma type_subst_identity: 
   "X\<sharp>T \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> = T"
   by (nominal_induct T avoiding: X U rule: ty.strong_induct)
     (simp_all add: fresh_atm abs_fresh)
 
 lemma type_substitution_lemma:  
   "X \<noteq> Y \<Longrightarrow> X\<sharp>L \<Longrightarrow> M[X \<mapsto> N]\<^sub>\<tau>[Y \<mapsto> L]\<^sub>\<tau> = M[Y \<mapsto> L]\<^sub>\<tau>[X \<mapsto> N[Y \<mapsto> L]\<^sub>\<tau>]\<^sub>\<tau>"
   by (nominal_induct M avoiding: X Y N L rule: ty.strong_induct)
     (auto simp: type_subst_fresh type_subst_identity)
 
 lemma type_subst_rename:
   "Y\<sharp>T \<Longrightarrow> ([(Y,X)]\<bullet>T)[Y \<mapsto> U]\<^sub>\<tau> = T[X \<mapsto> U]\<^sub>\<tau>"
   by (nominal_induct T avoiding: X Y U rule: ty.strong_induct)
     (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux)
 
 nominal_primrec
   subst_tyb :: "binding \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> binding" ("_[_ \<mapsto> _]\<^sub>b" [100,100,100] 100)
 where
   "(TVarB X U)[Y \<mapsto> T]\<^sub>b = TVarB X (U[Y \<mapsto> T]\<^sub>\<tau>)"
 | "(VarB  X U)[Y \<mapsto> T]\<^sub>b =  VarB X (U[Y \<mapsto> T]\<^sub>\<tau>)"
 by auto
 
 lemma binding_subst_fresh:
   fixes X::"tyvrs"
   assumes "X\<sharp>a"
   and     "X\<sharp>P"
   shows "X\<sharp>a[Y \<mapsto> P]\<^sub>b"
 using assms
 by (nominal_induct a rule: binding.strong_induct)
    (auto simp: type_subst_fresh)
 
 lemma binding_subst_identity: 
   shows "X\<sharp>B \<Longrightarrow> B[X \<mapsto> U]\<^sub>b = B"
 by (induct B rule: binding.induct)
    (simp_all add: fresh_atm type_subst_identity)
 
 primrec subst_tyc :: "env \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> env" ("_[_ \<mapsto> _]\<^sub>e" [100,100,100] 100) where
   "([])[Y \<mapsto> T]\<^sub>e= []"
 | "(B#\<Gamma>)[Y \<mapsto> T]\<^sub>e = (B[Y \<mapsto> T]\<^sub>b)#(\<Gamma>[Y \<mapsto> T]\<^sub>e)"
 
 lemma ctxt_subst_fresh':
   fixes X::"tyvrs"
   assumes "X\<sharp>\<Gamma>"
   and     "X\<sharp>P"
   shows   "X\<sharp>\<Gamma>[Y \<mapsto> P]\<^sub>e"
 using assms
 by (induct \<Gamma>)
    (auto simp: fresh_list_cons binding_subst_fresh)
 
 lemma ctxt_subst_mem_TVarB: "TVarB X T \<in> set \<Gamma> \<Longrightarrow> TVarB X (T[Y \<mapsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<mapsto> U]\<^sub>e)"
   by (induct \<Gamma>) auto
 
 lemma ctxt_subst_mem_VarB: "VarB x T \<in> set \<Gamma> \<Longrightarrow> VarB x (T[Y \<mapsto> U]\<^sub>\<tau>) \<in> set (\<Gamma>[Y \<mapsto> U]\<^sub>e)"
   by (induct \<Gamma>) auto
 
 lemma ctxt_subst_identity: "X\<sharp>\<Gamma> \<Longrightarrow> \<Gamma>[X \<mapsto> U]\<^sub>e = \<Gamma>"
   by (induct \<Gamma>) (simp_all add: fresh_list_cons binding_subst_identity)
 
 lemma ctxt_subst_append: "(\<Delta> @ \<Gamma>)[X \<mapsto> T]\<^sub>e = \<Delta>[X \<mapsto> T]\<^sub>e @ \<Gamma>[X \<mapsto> T]\<^sub>e"
   by (induct \<Delta>) simp_all
 
 nominal_primrec
    subst_trm :: "trm \<Rightarrow> vrs \<Rightarrow> trm \<Rightarrow> trm"  ("_[_ \<mapsto> _]" [300, 0, 0] 300)
 where
   "(Var x)[y \<mapsto> t'] = (if x=y then t' else (Var x))"
 | "(t1 \<cdot> t2)[y \<mapsto> t'] = t1[y \<mapsto> t'] \<cdot> t2[y \<mapsto> t']"
 | "(t \<cdot>\<^sub>\<tau> T)[y \<mapsto> t'] = t[y \<mapsto> t'] \<cdot>\<^sub>\<tau> T"
 | "X\<sharp>(T,t') \<Longrightarrow> (\<lambda>X<:T. t)[y \<mapsto> t'] = (\<lambda>X<:T. t[y \<mapsto> t'])" 
 | "x\<sharp>(y,t') \<Longrightarrow> (\<lambda>x:T. t)[y \<mapsto> t'] = (\<lambda>x:T. t[y \<mapsto> t'])"
-apply(finite_guess)+
-apply(rule TrueI)+
-apply(simp add: abs_fresh)+
-apply(fresh_guess add: ty_vrs_fresh abs_fresh)+
-done
+  by (finite_guess | simp add: abs_fresh | fresh_guess add: ty_vrs_fresh abs_fresh)+
 
 lemma subst_trm_fresh_tyvar:
   fixes X::"tyvrs"
   shows "X\<sharp>t \<Longrightarrow> X\<sharp>u \<Longrightarrow> X\<sharp>t[x \<mapsto> u]"
   by (nominal_induct t avoiding: x u rule: trm.strong_induct)
     (auto simp: abs_fresh)
 
 lemma subst_trm_fresh_var: 
   "x\<sharp>u \<Longrightarrow> x\<sharp>t[x \<mapsto> u]"
   by (nominal_induct t avoiding: x u rule: trm.strong_induct)
     (simp_all add: abs_fresh fresh_atm ty_vrs_fresh)
 
 lemma subst_trm_eqvt[eqvt]:
   fixes pi::"tyvrs prm" 
   and   t::"trm"
   shows "pi\<bullet>(t[x \<mapsto> u]) = (pi\<bullet>t)[(pi\<bullet>x) \<mapsto> (pi\<bullet>u)]"
   by (nominal_induct t avoiding: x u rule: trm.strong_induct)
      (perm_simp add: fresh_left)+
 
 lemma subst_trm_eqvt'[eqvt]:
   fixes pi::"vrs prm" 
   and   t::"trm"
   shows "pi\<bullet>(t[x \<mapsto> u]) = (pi\<bullet>t)[(pi\<bullet>x) \<mapsto> (pi\<bullet>u)]"
   by (nominal_induct t avoiding: x u rule: trm.strong_induct)
      (perm_simp add: fresh_left)+
 
 lemma subst_trm_rename:
   "y\<sharp>t \<Longrightarrow> ([(y, x)] \<bullet> t)[y \<mapsto> u] = t[x \<mapsto> u]"
   by (nominal_induct t avoiding: x y u rule: trm.strong_induct)
     (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux ty_vrs_fresh perm_fresh_fresh)
 
 nominal_primrec (freshness_context: "T2::ty")
   subst_trm_ty :: "trm \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> trm"  ("_[_ \<mapsto>\<^sub>\<tau> _]" [300, 0, 0] 300)
 where
   "(Var x)[Y \<mapsto>\<^sub>\<tau> T2] = Var x"
 | "(t1 \<cdot> t2)[Y \<mapsto>\<^sub>\<tau> T2] = t1[Y \<mapsto>\<^sub>\<tau> T2] \<cdot> t2[Y \<mapsto>\<^sub>\<tau> T2]"
 | "(t1 \<cdot>\<^sub>\<tau> T)[Y \<mapsto>\<^sub>\<tau> T2] = t1[Y \<mapsto>\<^sub>\<tau> T2] \<cdot>\<^sub>\<tau> T[Y \<mapsto> T2]\<^sub>\<tau>"
 | "X\<sharp>(Y,T,T2) \<Longrightarrow> (\<lambda>X<:T. t)[Y \<mapsto>\<^sub>\<tau> T2] = (\<lambda>X<:T[Y \<mapsto> T2]\<^sub>\<tau>. t[Y \<mapsto>\<^sub>\<tau> T2])" 
 | "(\<lambda>x:T. t)[Y \<mapsto>\<^sub>\<tau> T2] = (\<lambda>x:T[Y \<mapsto> T2]\<^sub>\<tau>. t[Y \<mapsto>\<^sub>\<tau> T2])"
 apply(finite_guess | simp add: abs_fresh ty_vrs_fresh type_subst_fresh)+
 apply(fresh_guess add: ty_vrs_fresh abs_fresh)+
 done
 
 lemma subst_trm_ty_fresh:
   fixes X::"tyvrs"
   shows "X\<sharp>t \<Longrightarrow> X\<sharp>T \<Longrightarrow> X\<sharp>t[Y \<mapsto>\<^sub>\<tau> T]"
   by (nominal_induct t avoiding: Y T rule: trm.strong_induct)
     (auto simp: abs_fresh type_subst_fresh)
 
 lemma subst_trm_ty_fresh':
   "X\<sharp>T \<Longrightarrow> X\<sharp>t[X \<mapsto>\<^sub>\<tau> T]"
   by (nominal_induct t avoiding: X T rule: trm.strong_induct)
     (simp_all add: abs_fresh fresh_type_subst_fresh fresh_atm)
 
 lemma subst_trm_ty_eqvt[eqvt]:
   fixes pi::"tyvrs prm" 
   and   t::"trm"
   shows "pi\<bullet>(t[X \<mapsto>\<^sub>\<tau> T]) = (pi\<bullet>t)[(pi\<bullet>X) \<mapsto>\<^sub>\<tau> (pi\<bullet>T)]"
   by (nominal_induct t avoiding: X T rule: trm.strong_induct)
      (perm_simp add: fresh_bij subst_eqvt)+
 
 lemma subst_trm_ty_eqvt'[eqvt]:
   fixes pi::"vrs prm" 
   and   t::"trm"
   shows "pi\<bullet>(t[X \<mapsto>\<^sub>\<tau> T]) = (pi\<bullet>t)[(pi\<bullet>X) \<mapsto>\<^sub>\<tau> (pi\<bullet>T)]"
   by (nominal_induct t avoiding: X T rule: trm.strong_induct)
      (perm_simp add: fresh_left subst_eqvt')+
 
 lemma subst_trm_ty_rename:
   "Y\<sharp>t \<Longrightarrow> ([(Y, X)] \<bullet> t)[Y \<mapsto>\<^sub>\<tau> U] = t[X \<mapsto>\<^sub>\<tau> U]"
   by (nominal_induct t avoiding: X Y U rule: trm.strong_induct)
     (simp_all add: fresh_atm calc_atm abs_fresh fresh_aux type_subst_rename)
 
 section \<open>Subtyping-Relation\<close>
 
 text \<open>The definition for the subtyping-relation follows quite closely what is written 
   in the POPLmark-paper, except for the premises dealing with well-formed contexts and 
   the freshness constraint \<^term>\<open>X\<sharp>\<Gamma>\<close> in the \<open>S_Forall\<close>-rule. (The freshness
   constraint is specific to the \emph{nominal approach}. Note, however, that the constraint
   does \emph{not} make the subtyping-relation ``partial"\ldots because we work over
   $\alpha$-equivalence classes.)\<close>
 
 inductive 
   subtype_of :: "env \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool"   ("_\<turnstile>_<:_" [100,100,100] 100)
 where
   SA_Top[intro]:    "\<lbrakk>\<turnstile> \<Gamma> ok; S closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: Top"
 | SA_refl_TVar[intro]:   "\<lbrakk>\<turnstile> \<Gamma> ok; X \<in> ty_dom \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Tvar X <: Tvar X"
 | SA_trans_TVar[intro]:    "\<lbrakk>(TVarB X S) \<in> set \<Gamma>; \<Gamma> \<turnstile> S <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (Tvar X) <: T"
 | SA_arrow[intro]:  "\<lbrakk>\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1; \<Gamma> \<turnstile> S\<^sub>2 <: T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (S\<^sub>1 \<rightarrow> S\<^sub>2) <: (T\<^sub>1 \<rightarrow> T\<^sub>2)" 
 | SA_all[intro]: "\<lbrakk>\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1; ((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> S\<^sub>2 <: T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: (\<forall>X<:T\<^sub>1. T\<^sub>2)"
 
 lemma subtype_implies_ok:
   fixes X::"tyvrs"
   assumes a: "\<Gamma> \<turnstile> S <: T"
   shows "\<turnstile> \<Gamma> ok"  
 using a by (induct) (auto)
 
 lemma subtype_implies_closed:
   assumes a: "\<Gamma> \<turnstile> S <: T"
   shows "S closed_in \<Gamma> \<and> T closed_in \<Gamma>"
 using a
 proof (induct)
   case (SA_Top \<Gamma> S)
   have "Top closed_in \<Gamma>" by (simp add: closed_in_def ty.supp)
   moreover
   have "S closed_in \<Gamma>" by fact
   ultimately show "S closed_in \<Gamma> \<and> Top closed_in \<Gamma>" by simp
 next
   case (SA_trans_TVar X S \<Gamma> T)
   have "(TVarB X S)\<in>set \<Gamma>" by fact
   hence "X \<in> ty_dom \<Gamma>" by (rule ty_dom_inclusion)
   hence "(Tvar X) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp supp_atm)
   moreover
   have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by fact
   hence "T closed_in \<Gamma>" by force
   ultimately show "(Tvar X) closed_in \<Gamma> \<and> T closed_in \<Gamma>" by simp
 qed (auto simp: closed_in_def ty.supp supp_atm abs_supp)
 
 lemma subtype_implies_fresh:
   fixes X::"tyvrs"
   assumes a1: "\<Gamma> \<turnstile> S <: T"
   and     a2: "X\<sharp>\<Gamma>"
   shows "X\<sharp>S \<and> X\<sharp>T"  
 proof -
   from a1 have "\<turnstile> \<Gamma> ok" by (rule subtype_implies_ok)
   with a2 have "X\<sharp>ty_dom(\<Gamma>)" by (simp add: fresh_dom)
   moreover
   from a1 have "S closed_in \<Gamma> \<and> T closed_in \<Gamma>" by (rule subtype_implies_closed)
   hence "supp S \<subseteq> ((supp (ty_dom \<Gamma>))::tyvrs set)" 
     and "supp T \<subseteq> ((supp (ty_dom \<Gamma>))::tyvrs set)" by (simp_all add: ty_dom_supp closed_in_def)
   ultimately show "X\<sharp>S \<and> X\<sharp>T" by (force simp: supp_prod fresh_def)
 qed
 
 lemma valid_ty_dom_fresh:
   fixes X::"tyvrs"
   assumes valid: "\<turnstile> \<Gamma> ok"
   shows "X\<sharp>(ty_dom \<Gamma>) = X\<sharp>\<Gamma>" 
   using valid
 proof induct
   case valid_nil
   then show ?case by auto
 next
   case (valid_consT \<Gamma> X T)
   then show ?case
     by (auto simp: fresh_list_cons closed_in_fresh
      fresh_fin_insert [OF pt_tyvrs_inst at_tyvrs_inst fs_tyvrs_inst] finite_doms)
 next
   case (valid_cons \<Gamma> x T)
   then show ?case
     using fresh_atm by (auto simp: fresh_list_cons closed_in_fresh)
 qed
 
 equivariance subtype_of
 
 nominal_inductive subtype_of
   apply (simp_all add: abs_fresh)
   apply (fastforce simp: valid_ty_dom_fresh dest: subtype_implies_ok)
   apply (force simp: closed_in_fresh dest: subtype_implies_closed subtype_implies_ok)+
   done
 
 section \<open>Reflexivity of Subtyping\<close>
 
 lemma subtype_reflexivity:
   assumes a: "\<turnstile> \<Gamma> ok"
   and b: "T closed_in \<Gamma>"
   shows "\<Gamma> \<turnstile> T <: T"
 using a b
 proof(nominal_induct T avoiding: \<Gamma> rule: ty.strong_induct)
   case (Forall X T\<^sub>1 T\<^sub>2)
   have ih_T\<^sub>1: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^sub>1 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^sub>1 <: T\<^sub>1" by fact 
   have ih_T\<^sub>2: "\<And>\<Gamma>. \<lbrakk>\<turnstile> \<Gamma> ok; T\<^sub>2 closed_in \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>2" by fact
   have fresh_cond: "X\<sharp>\<Gamma>" by fact
   hence fresh_ty_dom: "X\<sharp>(ty_dom \<Gamma>)" by (simp add: fresh_dom)
   have "(\<forall>X<:T\<^sub>2. T\<^sub>1) closed_in \<Gamma>" by fact
   hence closed\<^sub>T2: "T\<^sub>2 closed_in \<Gamma>" and closed\<^sub>T1: "T\<^sub>1 closed_in ((TVarB  X T\<^sub>2)#\<Gamma>)" 
     by (auto simp: closed_in_def ty.supp abs_supp)
   have ok: "\<turnstile> \<Gamma> ok" by fact  
   hence ok': "\<turnstile> ((TVarB X T\<^sub>2)#\<Gamma>) ok" using closed\<^sub>T2 fresh_ty_dom by simp
   have "\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>2" using ih_T\<^sub>2 closed\<^sub>T2 ok by simp
   moreover
   have "((TVarB X T\<^sub>2)#\<Gamma>) \<turnstile> T\<^sub>1 <: T\<^sub>1" using ih_T\<^sub>1 closed\<^sub>T1 ok' by simp
   ultimately show "\<Gamma> \<turnstile> (\<forall>X<:T\<^sub>2. T\<^sub>1) <: (\<forall>X<:T\<^sub>2. T\<^sub>1)" using fresh_cond 
     by (simp add: subtype_of.SA_all)
 qed (auto simp: closed_in_def ty.supp supp_atm)
 
 lemma subtype_reflexivity_semiautomated:
   assumes a: "\<turnstile> \<Gamma> ok"
   and     b: "T closed_in \<Gamma>"
   shows "\<Gamma> \<turnstile> T <: T"
 using a b
 apply(nominal_induct T avoiding: \<Gamma> rule: ty.strong_induct)
 apply(auto simp: ty.supp abs_supp supp_atm closed_in_def)
   \<comment> \<open>Too bad that this instantiation cannot be found automatically by
   \isakeyword{auto}; \isakeyword{blast} would find it if we had not used 
   an explicit definition for \<open>closed_in_def\<close>.\<close>
 apply(drule_tac x="(TVarB tyvrs ty2)#\<Gamma>" in meta_spec)
 apply(force dest: fresh_dom simp add: closed_in_def)
 done
 
 section \<open>Weakening\<close>
 
 text \<open>In order to prove weakening we introduce the notion of a type-context extending 
   another. This generalization seems to make the proof for weakening to be
   smoother than if we had strictly adhered to the version in the POPLmark-paper.\<close>
 
 definition extends :: "env \<Rightarrow> env \<Rightarrow> bool" ("_ extends _" [100,100] 100) where
   "\<Delta> extends \<Gamma> \<equiv> \<forall>X Q. (TVarB X Q)\<in>set \<Gamma> \<longrightarrow> (TVarB X Q)\<in>set \<Delta>"
 
 lemma extends_ty_dom:
   assumes "\<Delta> extends \<Gamma>"
   shows "ty_dom \<Gamma> \<subseteq> ty_dom \<Delta>"
   using assms
   by (meson extends_def subsetI ty_dom_existence ty_dom_inclusion) 
 
 lemma extends_closed:
   assumes "T closed_in \<Gamma>" and "\<Delta> extends \<Gamma>"
   shows "T closed_in \<Delta>"
   by (meson assms closed_in_def extends_ty_dom order.trans)
 
 lemma extends_memb:
   assumes a: "\<Delta> extends \<Gamma>"
   and b: "(TVarB X T) \<in> set \<Gamma>"
   shows "(TVarB X T) \<in> set \<Delta>"
   using a b by (simp add: extends_def)
 
 lemma weakening:
   assumes a: "\<Gamma> \<turnstile> S <: T"
   and b: "\<turnstile> \<Delta> ok"
   and c: "\<Delta> extends \<Gamma>"
   shows "\<Delta> \<turnstile> S <: T"
   using a b c 
 proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of.strong_induct)
   case (SA_Top \<Gamma> S) 
   have lh_drv_prem: "S closed_in \<Gamma>" by fact
   have "\<turnstile> \<Delta> ok" by fact
   moreover
   have "\<Delta> extends \<Gamma>" by fact
   hence "S closed_in \<Delta>" using lh_drv_prem by (simp only: extends_closed)
   ultimately show "\<Delta> \<turnstile> S <: Top" by force
 next 
   case (SA_trans_TVar X S \<Gamma> T)
   have lh_drv_prem: "(TVarB X S) \<in> set \<Gamma>" by fact
   have ih: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> S <: T" by fact
   have ok: "\<turnstile> \<Delta> ok" by fact
   have extends: "\<Delta> extends \<Gamma>" by fact
   have "(TVarB X S) \<in> set \<Delta>" using lh_drv_prem extends by (simp only: extends_memb)
   moreover
   have "\<Delta> \<turnstile> S <: T" using ok extends ih by simp
   ultimately show "\<Delta> \<turnstile> Tvar X <: T" using ok by force
 next
   case (SA_refl_TVar \<Gamma> X)
   have lh_drv_prem: "X \<in> ty_dom \<Gamma>" by fact
   have "\<turnstile> \<Delta> ok" by fact
   moreover
   have "\<Delta> extends \<Gamma>" by fact
   hence "X \<in> ty_dom \<Delta>" using lh_drv_prem by (force dest: extends_ty_dom)
   ultimately show "\<Delta> \<turnstile> Tvar X <: Tvar X" by force
 next 
   case (SA_arrow \<Gamma> T\<^sub>1 S\<^sub>1 S\<^sub>2 T\<^sub>2) thus "\<Delta> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T\<^sub>1 \<rightarrow> T\<^sub>2" by blast
 next
   case (SA_all \<Gamma> T\<^sub>1 S\<^sub>1 X S\<^sub>2 T\<^sub>2)
   have fresh_cond: "X\<sharp>\<Delta>" by fact
   hence fresh_dom: "X\<sharp>(ty_dom \<Delta>)" by (simp add: fresh_dom)
   have ih\<^sub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^sub>1 <: S\<^sub>1" by fact
   have ih\<^sub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((TVarB X T\<^sub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^sub>2 <: T\<^sub>2" by fact
   have lh_drv_prem: "\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1" by fact
   hence closed\<^sub>T1: "T\<^sub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   have ok: "\<turnstile> \<Delta> ok" by fact
   have ext: "\<Delta> extends \<Gamma>" by fact
   have "T\<^sub>1 closed_in \<Delta>" using ext closed\<^sub>T1 by (simp only: extends_closed)
   hence "\<turnstile> ((TVarB X T\<^sub>1)#\<Delta>) ok" using fresh_dom ok by force   
   moreover 
   have "((TVarB X T\<^sub>1)#\<Delta>) extends ((TVarB X T\<^sub>1)#\<Gamma>)" using ext by (force simp: extends_def)
   ultimately have "((TVarB X T\<^sub>1)#\<Delta>) \<turnstile> S\<^sub>2 <: T\<^sub>2" using ih\<^sub>2 by simp
   moreover
   have "\<Delta> \<turnstile> T\<^sub>1 <: S\<^sub>1" using ok ext ih\<^sub>1 by simp 
   ultimately show "\<Delta> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: (\<forall>X<:T\<^sub>1. T\<^sub>2)" using ok by (force intro: SA_all)
 qed
 
 text \<open>In fact all ``non-binding" cases can be solved automatically:\<close>
 
 lemma weakening_more_automated:
   assumes a: "\<Gamma> \<turnstile> S <: T"
   and b: "\<turnstile> \<Delta> ok"
   and c: "\<Delta> extends \<Gamma>"
   shows "\<Delta> \<turnstile> S <: T"
   using a b c 
 proof (nominal_induct \<Gamma> S T avoiding: \<Delta> rule: subtype_of.strong_induct)
   case (SA_all \<Gamma> T\<^sub>1 S\<^sub>1 X S\<^sub>2 T\<^sub>2)
   have fresh_cond: "X\<sharp>\<Delta>" by fact
   hence fresh_dom: "X\<sharp>(ty_dom \<Delta>)" by (simp add: fresh_dom)
   have ih\<^sub>1: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends \<Gamma> \<Longrightarrow> \<Delta> \<turnstile> T\<^sub>1 <: S\<^sub>1" by fact
   have ih\<^sub>2: "\<And>\<Delta>. \<turnstile> \<Delta> ok \<Longrightarrow> \<Delta> extends ((TVarB X T\<^sub>1)#\<Gamma>) \<Longrightarrow> \<Delta> \<turnstile> S\<^sub>2 <: T\<^sub>2" by fact
   have lh_drv_prem: "\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1" by fact
   hence closed\<^sub>T1: "T\<^sub>1 closed_in \<Gamma>" by (simp add: subtype_implies_closed) 
   have ok: "\<turnstile> \<Delta> ok" by fact
   have ext: "\<Delta> extends \<Gamma>" by fact
   have "T\<^sub>1 closed_in \<Delta>" using ext closed\<^sub>T1 by (simp only: extends_closed)
   hence "\<turnstile> ((TVarB X T\<^sub>1)#\<Delta>) ok" using fresh_dom ok by force   
   moreover
   have "((TVarB X T\<^sub>1)#\<Delta>) extends ((TVarB X T\<^sub>1)#\<Gamma>)" using ext by (force simp: extends_def)
   ultimately have "((TVarB X T\<^sub>1)#\<Delta>) \<turnstile> S\<^sub>2 <: T\<^sub>2" using ih\<^sub>2 by simp
   moreover
   have "\<Delta> \<turnstile> T\<^sub>1 <: S\<^sub>1" using ok ext ih\<^sub>1 by simp 
   ultimately show "\<Delta> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: (\<forall>X<:T\<^sub>1. T\<^sub>2)" using ok by (force intro: SA_all)
 qed (blast intro: extends_closed extends_memb dest: extends_ty_dom)+
 
 section \<open>Transitivity and Narrowing\<close>
 
 text \<open>Some inversion lemmas that are needed in the transitivity and narrowing proof.\<close>
 
 declare ty.inject [simp add]
 
 inductive_cases S_TopE: "\<Gamma> \<turnstile> Top <: T"
 inductive_cases S_ArrowE_left: "\<Gamma> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T" 
 
 declare ty.inject [simp del]
 
 lemma S_ForallE_left:
   shows "\<lbrakk>\<Gamma> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: T; X\<sharp>\<Gamma>; X\<sharp>S\<^sub>1; X\<sharp>T\<rbrakk>
          \<Longrightarrow> T = Top \<or> (\<exists>T\<^sub>1 T\<^sub>2. T = (\<forall>X<:T\<^sub>1. T\<^sub>2) \<and> \<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1 \<and> ((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> S\<^sub>2 <: T\<^sub>2)"
   using subtype_of.strong_cases[where X="X"]
   by(force simp: abs_fresh ty.inject alpha)
 
 text \<open>Next we prove the transitivity and narrowing for the subtyping-relation. 
 The POPLmark-paper says the following:
 
 \begin{quote}
 \begin{lemma}[Transitivity and Narrowing] \
 \begin{enumerate}
 \item If \<^term>\<open>\<Gamma> \<turnstile> S<:Q\<close> and \<^term>\<open>\<Gamma> \<turnstile> Q<:T\<close>, then \<^term>\<open>\<Gamma> \<turnstile> S<:T\<close>.
 \item If \<open>\<Gamma>,X<:Q,\<Delta> \<turnstile> M<:N\<close> and \<^term>\<open>\<Gamma> \<turnstile> P<:Q\<close> then \<open>\<Gamma>,X<:P,\<Delta> \<turnstile> M<:N\<close>.
 \end{enumerate}
 \end{lemma}
 
 The two parts are proved simultaneously, by induction on the size
 of \<^term>\<open>Q\<close>.  The argument for part (2) assumes that part (1) has 
 been established already for the \<^term>\<open>Q\<close> in question; part (1) uses 
 part (2) only for strictly smaller \<^term>\<open>Q\<close>.
 \end{quote}
 
 For the induction on the size of \<^term>\<open>Q\<close>, we use the induction-rule 
 \<open>measure_induct_rule\<close>:
 
 \begin{center}
 @{thm measure_induct_rule[of "size_ty",no_vars]}
 \end{center}
 
 That means in order to show a property \<^term>\<open>P a\<close> for all \<^term>\<open>a\<close>, 
 the induct-rule requires to prove that for all \<^term>\<open>x\<close> \<^term>\<open>P x\<close> holds using the 
 assumption that for all \<^term>\<open>y\<close> whose size is strictly smaller than 
 that of \<^term>\<open>x\<close> the property \<^term>\<open>P y\<close> holds.\<close>
 
 lemma 
   shows subtype_transitivity: "\<Gamma>\<turnstile>S<:Q \<Longrightarrow> \<Gamma>\<turnstile>Q<:T \<Longrightarrow> \<Gamma>\<turnstile>S<:T" 
   and subtype_narrow: "(\<Delta>@[(TVarB X Q)]@\<Gamma>)\<turnstile>M<:N \<Longrightarrow> \<Gamma>\<turnstile>P<:Q \<Longrightarrow> (\<Delta>@[(TVarB X P)]@\<Gamma>)\<turnstile>M<:N"
 proof (induct Q arbitrary: \<Gamma> S T \<Delta> X P M N taking: "size_ty" rule: measure_induct_rule)
   case (less Q)
   have IH_trans:  
     "\<And>Q' \<Gamma> S T. \<lbrakk>size_ty Q' < size_ty Q; \<Gamma>\<turnstile>S<:Q'; \<Gamma>\<turnstile>Q'<:T\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>S<:T" by fact
   have IH_narrow:
     "\<And>Q' \<Delta> \<Gamma> X M N P. \<lbrakk>size_ty Q' < size_ty Q; (\<Delta>@[(TVarB X Q')]@\<Gamma>)\<turnstile>M<:N; \<Gamma>\<turnstile>P<:Q'\<rbrakk> 
     \<Longrightarrow> (\<Delta>@[(TVarB X P)]@\<Gamma>)\<turnstile>M<:N" by fact
 
   { fix \<Gamma> S T
     have "\<lbrakk>\<Gamma> \<turnstile> S <: Q; \<Gamma> \<turnstile> Q <: T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> S <: T" 
     proof (induct \<Gamma> S Q\<equiv>Q rule: subtype_of.induct) 
       case (SA_Top \<Gamma> S) 
       then have rh_drv: "\<Gamma> \<turnstile> Top <: T" by simp
       then have T_inst: "T = Top" by (auto elim: S_TopE)
       from \<open>\<turnstile> \<Gamma> ok\<close> and \<open>S closed_in \<Gamma>\<close>
       have "\<Gamma> \<turnstile> S <: Top" by auto
       then show "\<Gamma> \<turnstile> S <: T" using T_inst by simp 
     next
       case (SA_trans_TVar Y U \<Gamma>) 
       then have IH_inner: "\<Gamma> \<turnstile> U <: T" by simp
       have "(TVarB Y U) \<in> set \<Gamma>" by fact
       with IH_inner show "\<Gamma> \<turnstile> Tvar Y <: T" by auto
     next
       case (SA_refl_TVar \<Gamma> X) 
       then show "\<Gamma> \<turnstile> Tvar X <: T" by simp
     next
       case (SA_arrow \<Gamma> Q\<^sub>1 S\<^sub>1 S\<^sub>2 Q\<^sub>2) 
       then have rh_drv: "\<Gamma> \<turnstile> Q\<^sub>1 \<rightarrow> Q\<^sub>2 <: T" by simp
       from \<open>Q\<^sub>1 \<rightarrow> Q\<^sub>2 = Q\<close> 
       have Q\<^sub>12_less: "size_ty Q\<^sub>1 < size_ty Q" "size_ty Q\<^sub>2 < size_ty Q" by auto
       have lh_drv_prm\<^sub>1: "\<Gamma> \<turnstile> Q\<^sub>1 <: S\<^sub>1" by fact
       have lh_drv_prm\<^sub>2: "\<Gamma> \<turnstile> S\<^sub>2 <: Q\<^sub>2" by fact      
       from rh_drv have "T=Top \<or> (\<exists>T\<^sub>1 T\<^sub>2. T=T\<^sub>1\<rightarrow>T\<^sub>2 \<and> \<Gamma>\<turnstile>T\<^sub>1<:Q\<^sub>1 \<and> \<Gamma>\<turnstile>Q\<^sub>2<:T\<^sub>2)" 
         by (auto elim: S_ArrowE_left)
       moreover
       have "S\<^sub>1 closed_in \<Gamma>" and "S\<^sub>2 closed_in \<Gamma>" 
         using lh_drv_prm\<^sub>1 lh_drv_prm\<^sub>2 by (simp_all add: subtype_implies_closed)
       hence "(S\<^sub>1 \<rightarrow> S\<^sub>2) closed_in \<Gamma>" by (simp add: closed_in_def ty.supp)
       moreover
       have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
       moreover
       { assume "\<exists>T\<^sub>1 T\<^sub>2. T = T\<^sub>1\<rightarrow>T\<^sub>2 \<and> \<Gamma> \<turnstile> T\<^sub>1 <: Q\<^sub>1 \<and> \<Gamma> \<turnstile> Q\<^sub>2 <: T\<^sub>2"
         then obtain T\<^sub>1 T\<^sub>2 
           where T_inst: "T = T\<^sub>1 \<rightarrow> T\<^sub>2" 
           and   rh_drv_prm\<^sub>1: "\<Gamma> \<turnstile> T\<^sub>1 <: Q\<^sub>1"
           and   rh_drv_prm\<^sub>2: "\<Gamma> \<turnstile> Q\<^sub>2 <: T\<^sub>2" by force
         from IH_trans[of "Q\<^sub>1"] 
         have "\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1" using Q\<^sub>12_less rh_drv_prm\<^sub>1 lh_drv_prm\<^sub>1 by simp 
         moreover
         from IH_trans[of "Q\<^sub>2"] 
         have "\<Gamma> \<turnstile> S\<^sub>2 <: T\<^sub>2" using Q\<^sub>12_less rh_drv_prm\<^sub>2 lh_drv_prm\<^sub>2 by simp
         ultimately have "\<Gamma> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T\<^sub>1 \<rightarrow> T\<^sub>2" by auto
         then have "\<Gamma> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T" using T_inst by simp
       }
       ultimately show "\<Gamma> \<turnstile> S\<^sub>1 \<rightarrow> S\<^sub>2 <: T" by blast
     next
       case (SA_all \<Gamma> Q\<^sub>1 S\<^sub>1 X S\<^sub>2 Q\<^sub>2) 
       then have rh_drv: "\<Gamma> \<turnstile> (\<forall>X<:Q\<^sub>1. Q\<^sub>2) <: T" by simp
       have lh_drv_prm\<^sub>1: "\<Gamma> \<turnstile> Q\<^sub>1 <: S\<^sub>1" by fact
       have lh_drv_prm\<^sub>2: "((TVarB X Q\<^sub>1)#\<Gamma>) \<turnstile> S\<^sub>2 <: Q\<^sub>2" by fact
       then have "X\<sharp>\<Gamma>" by (force dest: subtype_implies_ok simp add: valid_ty_dom_fresh)
       then have fresh_cond: "X\<sharp>\<Gamma>" "X\<sharp>Q\<^sub>1" "X\<sharp>T" using rh_drv lh_drv_prm\<^sub>1 
         by (simp_all add: subtype_implies_fresh)
       from rh_drv 
       have "T = Top \<or> 
           (\<exists>T\<^sub>1 T\<^sub>2. T = (\<forall>X<:T\<^sub>1. T\<^sub>2) \<and> \<Gamma> \<turnstile> T\<^sub>1 <: Q\<^sub>1 \<and> ((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> Q\<^sub>2 <: T\<^sub>2)" 
         using fresh_cond by (simp add: S_ForallE_left)
       moreover
       have "S\<^sub>1 closed_in \<Gamma>" and "S\<^sub>2 closed_in ((TVarB X Q\<^sub>1)#\<Gamma>)" 
         using lh_drv_prm\<^sub>1 lh_drv_prm\<^sub>2 by (simp_all add: subtype_implies_closed)
       then have "(\<forall>X<:S\<^sub>1. S\<^sub>2) closed_in \<Gamma>" by (force simp: closed_in_def ty.supp abs_supp)
       moreover
       have "\<turnstile> \<Gamma> ok" using rh_drv by (rule subtype_implies_ok)
       moreover
       { assume "\<exists>T\<^sub>1 T\<^sub>2. T=(\<forall>X<:T\<^sub>1. T\<^sub>2) \<and> \<Gamma>\<turnstile>T\<^sub>1<:Q\<^sub>1 \<and> ((TVarB X T\<^sub>1)#\<Gamma>)\<turnstile>Q\<^sub>2<:T\<^sub>2"
         then obtain T\<^sub>1 T\<^sub>2 
           where T_inst: "T = (\<forall>X<:T\<^sub>1. T\<^sub>2)" 
           and   rh_drv_prm\<^sub>1: "\<Gamma> \<turnstile> T\<^sub>1 <: Q\<^sub>1" 
           and   rh_drv_prm\<^sub>2:"((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> Q\<^sub>2 <: T\<^sub>2" by force
         have "(\<forall>X<:Q\<^sub>1. Q\<^sub>2) = Q" by fact 
         then have Q\<^sub>12_less: "size_ty Q\<^sub>1 < size_ty Q" "size_ty Q\<^sub>2 < size_ty Q" 
           using fresh_cond by auto
         from IH_trans[of "Q\<^sub>1"] 
         have "\<Gamma> \<turnstile> T\<^sub>1 <: S\<^sub>1" using lh_drv_prm\<^sub>1 rh_drv_prm\<^sub>1 Q\<^sub>12_less by blast
         moreover
         from IH_narrow[of "Q\<^sub>1" "[]"] 
         have "((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> S\<^sub>2 <: Q\<^sub>2" using Q\<^sub>12_less lh_drv_prm\<^sub>2 rh_drv_prm\<^sub>1 by simp
         with IH_trans[of "Q\<^sub>2"] 
         have "((TVarB X T\<^sub>1)#\<Gamma>) \<turnstile> S\<^sub>2 <: T\<^sub>2" using Q\<^sub>12_less rh_drv_prm\<^sub>2 by simp
         ultimately have "\<Gamma> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: (\<forall>X<:T\<^sub>1. T\<^sub>2)"
           using fresh_cond by (simp add: subtype_of.SA_all)
         hence "\<Gamma> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: T" using T_inst by simp
       }
       ultimately show "\<Gamma> \<turnstile> (\<forall>X<:S\<^sub>1. S\<^sub>2) <: T" by blast
     qed
   } note transitivity_lemma = this  
 
   { \<comment> \<open>The transitivity proof is now by the auxiliary lemma.\<close>
     case 1 
     from \<open>\<Gamma> \<turnstile> S <: Q\<close> and \<open>\<Gamma> \<turnstile> Q <: T\<close>
     show "\<Gamma> \<turnstile> S <: T" by (rule transitivity_lemma) 
   next 
     case 2
     from \<open>(\<Delta>@[(TVarB X Q)]@\<Gamma>) \<turnstile> M <: N\<close> 
       and \<open>\<Gamma> \<turnstile> P<:Q\<close> 
     show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> M <: N" 
     proof (induct "\<Delta>@[(TVarB X Q)]@\<Gamma>" M N arbitrary: \<Gamma> X \<Delta> rule: subtype_of.induct) 
       case (SA_Top S \<Gamma> X \<Delta>)
       from \<open>\<Gamma> \<turnstile> P <: Q\<close>
       have "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
       with \<open>\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok\<close> have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok"
         by (simp add: replace_type)
       moreover
       from \<open>S closed_in (\<Delta>@[(TVarB X Q)]@\<Gamma>)\<close> have "S closed_in (\<Delta>@[(TVarB X P)]@\<Gamma>)" 
         by (simp add: closed_in_def doms_append)
       ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: Top" by (simp add: subtype_of.SA_Top)
     next
       case (SA_trans_TVar Y S N \<Gamma> X \<Delta>) 
       then have IH_inner: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> S <: N"
         and lh_drv_prm: "(TVarB Y S) \<in> set (\<Delta>@[(TVarB X Q)]@\<Gamma>)"
         and rh_drv: "\<Gamma> \<turnstile> P<:Q"
         and ok\<^sub>Q: "\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok" by (simp_all add: subtype_implies_ok)
       then have ok\<^sub>P: "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok" by (simp add: subtype_implies_ok) 
       show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N"
       proof (cases "X=Y")
         case False
         have "X\<noteq>Y" by fact
         hence "(TVarB Y S)\<in>set (\<Delta>@[(TVarB X P)]@\<Gamma>)" using lh_drv_prm by (simp add:binding.inject)
         with IH_inner show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" by (simp add: subtype_of.SA_trans_TVar)
       next
         case True
         have memb\<^sub>XQ: "(TVarB X Q)\<in>set (\<Delta>@[(TVarB X Q)]@\<Gamma>)" by simp
         have memb\<^sub>XP: "(TVarB X P)\<in>set (\<Delta>@[(TVarB X P)]@\<Gamma>)" by simp
         have eq: "X=Y" by fact 
         hence "S=Q" using ok\<^sub>Q lh_drv_prm memb\<^sub>XQ by (simp only: uniqueness_of_ctxt)
         hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q <: N" using IH_inner by simp
         moreover
         have "(\<Delta>@[(TVarB X P)]@\<Gamma>) extends \<Gamma>" by (simp add: extends_def)
         hence "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: Q" using rh_drv ok\<^sub>P by (simp only: weakening)
         ultimately have "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> P <: N" by (simp add: transitivity_lemma) 
         then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: N" using memb\<^sub>XP eq by auto
       qed
     next
       case (SA_refl_TVar Y \<Gamma> X \<Delta>)
       from \<open>\<Gamma> \<turnstile> P <: Q\<close>
       have "P closed_in \<Gamma>" by (simp add: subtype_implies_closed)
       with \<open>\<turnstile> (\<Delta>@[(TVarB X Q)]@\<Gamma>) ok\<close> have "\<turnstile> (\<Delta>@[(TVarB X P)]@\<Gamma>) ok"
         by (simp add: replace_type)
       moreover
       from \<open>Y \<in> ty_dom (\<Delta>@[(TVarB X Q)]@\<Gamma>)\<close> have "Y \<in> ty_dom (\<Delta>@[(TVarB X P)]@\<Gamma>)"
         by (simp add: doms_append)
       ultimately show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Tvar Y <: Tvar Y" by (simp add: subtype_of.SA_refl_TVar)
     next
       case (SA_arrow S\<^sub>1 Q\<^sub>1 Q\<^sub>2 S\<^sub>2 \<Gamma> X \<Delta>) 
       then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> Q\<^sub>1 \<rightarrow> Q\<^sub>2 <: S\<^sub>1 \<rightarrow> S\<^sub>2" by blast 
     next
       case (SA_all T\<^sub>1 S\<^sub>1 Y S\<^sub>2 T\<^sub>2 \<Gamma> X \<Delta>)
       have IH_inner\<^sub>1: "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> T\<^sub>1 <: S\<^sub>1" 
         and IH_inner\<^sub>2: "(((TVarB Y T\<^sub>1)#\<Delta>)@[(TVarB X P)]@\<Gamma>) \<turnstile> S\<^sub>2 <: T\<^sub>2"
         by (fastforce intro: SA_all)+
       then show "(\<Delta>@[(TVarB X P)]@\<Gamma>) \<turnstile> (\<forall>Y<:S\<^sub>1. S\<^sub>2) <: (\<forall>Y<:T\<^sub>1. T\<^sub>2)" by auto
     qed
   } 
 qed
 
 section \<open>Typing\<close>
 
 inductive
   typing :: "env \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
 where
   T_Var[intro]: "\<lbrakk> VarB x T \<in> set \<Gamma>; \<turnstile> \<Gamma> ok \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
 | T_App[intro]: "\<lbrakk> \<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>1 \<rightarrow> T\<^sub>2; \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^sub>1 \<cdot> t\<^sub>2 : T\<^sub>2"
 | T_Abs[intro]: "\<lbrakk> VarB x T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>x:T\<^sub>1. t\<^sub>2) : T\<^sub>1 \<rightarrow> T\<^sub>2"
 | T_Sub[intro]: "\<lbrakk> \<Gamma> \<turnstile> t : S; \<Gamma> \<turnstile> S <: T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t : T"
 | T_TAbs[intro]:"\<lbrakk> TVarB X T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> (\<lambda>X<:T\<^sub>1. t\<^sub>2) : (\<forall>X<:T\<^sub>1. T\<^sub>2)"
 | T_TApp[intro]:"\<lbrakk>X\<sharp>(\<Gamma>,t\<^sub>1,T\<^sub>2); \<Gamma> \<turnstile> t\<^sub>1 : (\<forall>X<:T\<^sub>11. T\<^sub>12); \<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2 : (T\<^sub>12[X \<mapsto> T\<^sub>2]\<^sub>\<tau>)" 
 
 equivariance typing
 
 lemma better_T_TApp:
   assumes H1: "\<Gamma> \<turnstile> t\<^sub>1 : (\<forall>X<:T11. T12)"
   and H2: "\<Gamma> \<turnstile> T2 <: T11"
   shows "\<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T2 : (T12[X \<mapsto> T2]\<^sub>\<tau>)"
 proof -
   obtain Y::tyvrs where Y: "Y \<sharp> (X, T12, \<Gamma>, t\<^sub>1, T2)"
     by (rule exists_fresh) (rule fin_supp)
   then have "Y \<sharp> (\<Gamma>, t\<^sub>1, T2)" by simp
   moreover from Y have "(\<forall>X<:T11. T12) = (\<forall>Y<:T11. [(Y, X)] \<bullet> T12)"
     by (auto simp: ty.inject alpha' fresh_prod fresh_atm)
   with H1 have "\<Gamma> \<turnstile> t\<^sub>1 : (\<forall>Y<:T11. [(Y, X)] \<bullet> T12)" by simp
   ultimately have "\<Gamma> \<turnstile> t\<^sub>1 \<cdot>\<^sub>\<tau> T2 : (([(Y, X)] \<bullet> T12)[Y \<mapsto> T2]\<^sub>\<tau>)" using H2
     by (rule T_TApp)
   with Y show ?thesis by (simp add: type_subst_rename)
 qed
 
 lemma typing_ok:
   assumes "\<Gamma> \<turnstile> t : T"
   shows   "\<turnstile> \<Gamma> ok"
 using assms by (induct) (auto)
 
 nominal_inductive typing
 by (auto dest!: typing_ok intro: closed_in_fresh fresh_dom type_subst_fresh
     simp: abs_fresh fresh_type_subst_fresh ty_vrs_fresh valid_ty_dom_fresh fresh_trm_dom)
 
 lemma ok_imp_VarB_closed_in:
   assumes ok: "\<turnstile> \<Gamma> ok"
   shows "VarB x T \<in> set \<Gamma> \<Longrightarrow> T closed_in \<Gamma>" using ok
   by induct (auto simp: binding.inject closed_in_def)
 
 lemma tyvrs_of_subst: "tyvrs_of (B[X \<mapsto> T]\<^sub>b) = tyvrs_of B"
   by (nominal_induct B rule: binding.strong_induct) simp_all
 
 lemma ty_dom_subst: "ty_dom (\<Gamma>[X \<mapsto> T]\<^sub>e) = ty_dom \<Gamma>"
   by (induct \<Gamma>) (simp_all add: tyvrs_of_subst)
 
 lemma vrs_of_subst: "vrs_of (B[X \<mapsto> T]\<^sub>b) = vrs_of B"
   by (nominal_induct B rule: binding.strong_induct) simp_all
 
 lemma trm_dom_subst: "trm_dom (\<Gamma>[X \<mapsto> T]\<^sub>e) = trm_dom \<Gamma>"
   by (induct \<Gamma>) (simp_all add: vrs_of_subst)
 
 lemma subst_closed_in:
   "T closed_in (\<Delta> @ TVarB X S # \<Gamma>) \<Longrightarrow> U closed_in \<Gamma> \<Longrightarrow> T[X \<mapsto> U]\<^sub>\<tau> closed_in (\<Delta>[X \<mapsto> U]\<^sub>e @ \<Gamma>)"
 proof (nominal_induct T avoiding: X U \<Gamma> rule: ty.strong_induct)
   case (Tvar tyvrs)
   then show ?case
     by (auto simp add: closed_in_def ty.supp supp_atm doms_append ty_dom_subst)
 next
   case Top
   then show ?case
     using closed_in_def fresh_def by fastforce
 next
   case (Arrow ty1 ty2)
   then show ?case
     by (simp add: closed_in_def ty.supp)
 next
   case (Forall tyvrs ty1 ty2)
   then have "supp (ty1[X \<mapsto> U]\<^sub>\<tau>) \<subseteq> ty_dom (\<Delta>[X \<mapsto> U]\<^sub>e @ TVarB tyvrs ty2 # \<Gamma>)"
     apply (simp add: closed_in_def ty.supp abs_supp)
     by (metis Diff_subset_conv Un_left_commute doms_append(1) le_supI2 ty_dom.simps(2) tyvrs_of.simps(2))
   with Forall show ?case
     by (auto simp add: closed_in_def ty.supp abs_supp doms_append)
 qed
 
 lemmas subst_closed_in' = subst_closed_in [where \<Delta>="[]", simplified]
 
 lemma typing_closed_in:
   assumes "\<Gamma> \<turnstile> t : T"
   shows   "T closed_in \<Gamma>"
 using assms
 proof induct
   case (T_Var x T \<Gamma>)
   from \<open>\<turnstile> \<Gamma> ok\<close> and \<open>VarB x T \<in> set \<Gamma>\<close>
   show ?case by (rule ok_imp_VarB_closed_in)
 next
   case (T_App \<Gamma> t\<^sub>1 T\<^sub>1 T\<^sub>2 t\<^sub>2)
   then show ?case by (auto simp: ty.supp closed_in_def)
 next
   case (T_Abs x T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2)
   from \<open>VarB x T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close>
   have "T\<^sub>1 closed_in \<Gamma>" by (auto dest: typing_ok)
   with T_Abs show ?case by (auto simp: ty.supp closed_in_def)
 next
   case (T_Sub \<Gamma> t S T)
   from \<open>\<Gamma> \<turnstile> S <: T\<close> show ?case by (simp add: subtype_implies_closed)
 next
   case (T_TAbs X T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2)
   from \<open>TVarB X T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close>
   have "T\<^sub>1 closed_in \<Gamma>" by (auto dest: typing_ok)
   with T_TAbs show ?case by (auto simp: ty.supp closed_in_def abs_supp)
 next
   case (T_TApp X \<Gamma> t\<^sub>1 T2 T11 T12)
   then have "T12 closed_in (TVarB X T11 # \<Gamma>)"
     by (auto simp: closed_in_def ty.supp abs_supp)
   moreover from T_TApp have "T2 closed_in \<Gamma>"
     by (simp add: subtype_implies_closed)
   ultimately show ?case by (rule subst_closed_in')
 qed
 
 
 subsection \<open>Evaluation\<close>
 
 inductive
   val :: "trm \<Rightarrow> bool"
 where
   Abs[intro]:  "val (\<lambda>x:T. t)"
 | TAbs[intro]: "val (\<lambda>X<:T. t)"
 
 equivariance val
 
 inductive_cases val_inv_auto[elim]: 
   "val (Var x)" 
   "val (t1 \<cdot> t2)" 
   "val (t1 \<cdot>\<^sub>\<tau> t2)"
 
 inductive 
   eval :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longmapsto> _" [60,60] 60)
 where
   E_Abs         : "\<lbrakk> x \<sharp> v\<^sub>2; val v\<^sub>2 \<rbrakk> \<Longrightarrow> (\<lambda>x:T\<^sub>11. t\<^sub>12) \<cdot> v\<^sub>2 \<longmapsto> t\<^sub>12[x \<mapsto> v\<^sub>2]"
 | E_App1 [intro]: "t \<longmapsto> t' \<Longrightarrow> t \<cdot> u \<longmapsto> t' \<cdot> u"
 | E_App2 [intro]: "\<lbrakk> val v; t \<longmapsto> t' \<rbrakk> \<Longrightarrow> v \<cdot> t \<longmapsto> v \<cdot> t'"
 | E_TAbs        : "X \<sharp> (T\<^sub>11, T\<^sub>2) \<Longrightarrow> (\<lambda>X<:T\<^sub>11. t\<^sub>12) \<cdot>\<^sub>\<tau> T\<^sub>2 \<longmapsto> t\<^sub>12[X \<mapsto>\<^sub>\<tau> T\<^sub>2]"
 | E_TApp [intro]: "t \<longmapsto> t' \<Longrightarrow> t \<cdot>\<^sub>\<tau> T \<longmapsto> t' \<cdot>\<^sub>\<tau> T"
 
 lemma better_E_Abs[intro]:
   assumes H: "val v2"
   shows "(\<lambda>x:T11. t12) \<cdot> v2 \<longmapsto> t12[x \<mapsto> v2]"
 proof -
   obtain y::vrs where y: "y \<sharp> (x, t12, v2)" by (rule exists_fresh) (rule fin_supp)
   then have "y \<sharp> v2" by simp
   then have "(\<lambda>y:T11. [(y, x)] \<bullet> t12) \<cdot> v2 \<longmapsto> ([(y, x)] \<bullet> t12)[y \<mapsto> v2]" using H
     by (rule E_Abs)
   moreover from y have "(\<lambda>x:T11. t12) \<cdot> v2 = (\<lambda>y:T11. [(y, x)] \<bullet> t12) \<cdot> v2"
     by (auto simp: trm.inject alpha' fresh_prod fresh_atm)
   ultimately have "(\<lambda>x:T11. t12) \<cdot> v2 \<longmapsto> ([(y, x)] \<bullet> t12)[y \<mapsto> v2]"
     by simp
   with y show ?thesis by (simp add: subst_trm_rename)
 qed
 
 lemma better_E_TAbs[intro]: "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> t12[X \<mapsto>\<^sub>\<tau> T2]"
 proof -
   obtain Y::tyvrs where Y: "Y \<sharp> (X, t12, T11, T2)" by (rule exists_fresh) (rule fin_supp)
   then have "Y \<sharp> (T11, T2)" by simp
   then have "(\<lambda>Y<:T11. [(Y, X)] \<bullet> t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> ([(Y, X)] \<bullet> t12)[Y \<mapsto>\<^sub>\<tau> T2]"
     by (rule E_TAbs)
   moreover from Y have "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 = (\<lambda>Y<:T11. [(Y, X)] \<bullet> t12) \<cdot>\<^sub>\<tau> T2"
     by (auto simp: trm.inject alpha' fresh_prod fresh_atm)
   ultimately have "(\<lambda>X<:T11. t12) \<cdot>\<^sub>\<tau> T2 \<longmapsto> ([(Y, X)] \<bullet> t12)[Y \<mapsto>\<^sub>\<tau> T2]"
     by simp
   with Y show ?thesis by (simp add: subst_trm_ty_rename)
 qed
 
 equivariance eval
 
 nominal_inductive eval
   by (simp_all add: abs_fresh ty_vrs_fresh subst_trm_fresh_tyvar
     subst_trm_fresh_var subst_trm_ty_fresh')
 
 inductive_cases eval_inv_auto[elim]: 
   "Var x \<longmapsto> t'" 
   "(\<lambda>x:T. t) \<longmapsto> t'" 
   "(\<lambda>X<:T. t) \<longmapsto> t'" 
 
 lemma ty_dom_cons:
   shows "ty_dom (\<Gamma>@[VarB X Q]@\<Delta>) = ty_dom (\<Gamma>@\<Delta>)"
 by (induct \<Gamma>) (auto)
 
 lemma closed_in_cons: 
   assumes "S closed_in (\<Gamma> @ VarB X Q # \<Delta>)"
   shows "S closed_in (\<Gamma>@\<Delta>)"
 using assms ty_dom_cons closed_in_def by auto
 
 lemma closed_in_weaken: "T closed_in (\<Delta> @ \<Gamma>) \<Longrightarrow> T closed_in (\<Delta> @ B # \<Gamma>)"
   by (auto simp: closed_in_def doms_append)
 
 lemma closed_in_weaken': "T closed_in \<Gamma> \<Longrightarrow> T closed_in (\<Delta> @ \<Gamma>)"
   by (auto simp: closed_in_def doms_append)
 
 lemma valid_subst:
   assumes ok: "\<turnstile> (\<Delta> @ TVarB X Q # \<Gamma>) ok"
   and closed: "P closed_in \<Gamma>"
   shows "\<turnstile> (\<Delta>[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" using ok closed
 proof (induct \<Delta>)
   case Nil
   then show ?case
     by auto
 next
   case (Cons a \<Delta>)
   then have *: "\<turnstile> (a # \<Delta> @ TVarB X Q # \<Gamma>) ok"
     by fastforce
   then show ?case
     apply (rule validE)
     using Cons
      apply (simp add: at_tyvrs_inst closed doms_append(1) finite_doms(1) fresh_fin_insert fs_tyvrs_inst pt_tyvrs_inst subst_closed_in ty_dom_subst)
     by (simp add: doms_append(2) subst_closed_in Cons.hyps closed trm_dom_subst)
 qed
 
 lemma ty_dom_vrs:
   shows "ty_dom (G @ [VarB x Q] @ D) = ty_dom (G @ D)"
   by (induct G) (auto)
 
 lemma valid_cons':
   assumes "\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok"
   shows "\<turnstile> (\<Gamma> @ \<Delta>) ok"
   using assms
 proof (induct "\<Gamma> @ VarB x Q # \<Delta>" arbitrary: \<Gamma> \<Delta>)
   case valid_nil
   have "[] = \<Gamma> @ VarB x Q # \<Delta>" by fact
   then have "False" by auto
   then show ?case by auto
 next
   case (valid_consT G X T)
   then show ?case
   proof (cases \<Gamma>)
     case Nil
     with valid_consT show ?thesis by simp
   next
     case (Cons b bs)
     with valid_consT
     have "\<turnstile> (bs @ \<Delta>) ok" by simp
     moreover from Cons and valid_consT have "X \<sharp> ty_dom (bs @ \<Delta>)"
       by (simp add: doms_append)
     moreover from Cons and valid_consT have "T closed_in (bs @ \<Delta>)"
       by (simp add: closed_in_def doms_append)
     ultimately have "\<turnstile> (TVarB X T # bs @ \<Delta>) ok"
       by (rule valid_rel.valid_consT)
     with Cons and valid_consT show ?thesis by simp
   qed
 next
   case (valid_cons G x T)
   then show ?case
   proof (cases \<Gamma>)
     case Nil
     with valid_cons show ?thesis by simp
   next
     case (Cons b bs)
     with valid_cons
     have "\<turnstile> (bs @ \<Delta>) ok" by simp
     moreover from Cons and valid_cons have "x \<sharp> trm_dom (bs @ \<Delta>)"
       by (simp add: doms_append finite_doms
         fresh_fin_insert [OF pt_vrs_inst at_vrs_inst fs_vrs_inst])
     moreover from Cons and valid_cons have "T closed_in (bs @ \<Delta>)"
       by (simp add: closed_in_def doms_append)
     ultimately have "\<turnstile> (VarB x T # bs @ \<Delta>) ok"
       by (rule valid_rel.valid_cons)
     with Cons and valid_cons show ?thesis by simp
   qed
 qed
   
 text \<open>A.5(6)\<close>
 
 lemma type_weaken:
   assumes "(\<Delta>@\<Gamma>) \<turnstile> t : T"
   and     "\<turnstile> (\<Delta> @ B # \<Gamma>) ok"
   shows   "(\<Delta> @ B # \<Gamma>) \<turnstile> t : T"
 using assms
 proof(nominal_induct "\<Delta> @ \<Gamma>" t T avoiding: \<Delta> \<Gamma> B rule: typing.strong_induct)
   case (T_Var x T)
   then show ?case by auto
 next
   case (T_App X t\<^sub>1 T\<^sub>2 T\<^sub>11 T\<^sub>12)
   then show ?case by force
 next
   case (T_Abs y T\<^sub>1 t\<^sub>2 T\<^sub>2 \<Delta> \<Gamma>)
   then have "VarB y T\<^sub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2" by simp
   then have closed: "T\<^sub>1 closed_in (\<Delta> @ \<Gamma>)"
     by (auto dest: typing_ok)
   have "\<turnstile> (VarB y T\<^sub>1 # \<Delta> @ B # \<Gamma>) ok"
     by (simp add: T_Abs closed closed_in_weaken fresh_list_append fresh_list_cons fresh_trm_dom)
   then have "\<turnstile> ((VarB y T\<^sub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp
   with _ have "(VarB y T\<^sub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2"
     by (rule T_Abs) simp
   then have "VarB y T\<^sub>1 # \<Delta> @ B # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2" by simp
   then show ?case by (rule typing.T_Abs)
 next
   case (T_Sub t S T \<Delta> \<Gamma>)
   from refl and \<open>\<turnstile> (\<Delta> @ B # \<Gamma>) ok\<close>
   have "\<Delta> @ B # \<Gamma> \<turnstile> t : S" by (rule T_Sub)
   moreover from  \<open>(\<Delta> @ \<Gamma>)\<turnstile>S<:T\<close> and \<open>\<turnstile> (\<Delta> @ B # \<Gamma>) ok\<close>
   have "(\<Delta> @ B # \<Gamma>)\<turnstile>S<:T"
     by (rule weakening) (simp add: extends_def T_Sub)
   ultimately show ?case by (rule typing.T_Sub)
 next
   case (T_TAbs X T\<^sub>1 t\<^sub>2 T\<^sub>2 \<Delta> \<Gamma>)
   from \<open>TVarB X T\<^sub>1 # \<Delta> @ \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close>
   have closed: "T\<^sub>1 closed_in (\<Delta> @ \<Gamma>)"
     by (auto dest: typing_ok)
   have "\<turnstile> (TVarB X T\<^sub>1 # \<Delta> @ B # \<Gamma>) ok"
     by (simp add: T_TAbs at_tyvrs_inst closed closed_in_weaken doms_append finite_doms finite_vrs
         fresh_dom fresh_fin_union fs_tyvrs_inst pt_tyvrs_inst tyvrs_fresh)
   then have "\<turnstile> ((TVarB X T\<^sub>1 # \<Delta>) @ B # \<Gamma>) ok" by simp
   with _ have "(TVarB X T\<^sub>1 # \<Delta>) @ B # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2"
     by (rule T_TAbs) simp
   then have "TVarB X T\<^sub>1 # \<Delta> @ B # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2" by simp
   then show ?case by (rule typing.T_TAbs)
 next
   case (T_TApp X t\<^sub>1 T2 T11 T12 \<Delta> \<Gamma>)
   have "\<Delta> @ B # \<Gamma> \<turnstile> t\<^sub>1 : (\<forall>X<:T11. T12)"
     by (rule T_TApp refl)+
   moreover from \<open>(\<Delta> @ \<Gamma>)\<turnstile>T2<:T11\<close> and \<open>\<turnstile> (\<Delta> @ B # \<Gamma>) ok\<close>
   have "(\<Delta> @ B # \<Gamma>)\<turnstile>T2<:T11"
     by (rule weakening) (simp add: extends_def T_TApp)
   ultimately show ?case by (rule better_T_TApp)
 qed
 
 lemma type_weaken':
  "\<Gamma> \<turnstile> t : T \<Longrightarrow>  \<turnstile> (\<Delta>@\<Gamma>) ok \<Longrightarrow> (\<Delta>@\<Gamma>) \<turnstile> t : T"
 proof (induct \<Delta>)
   case Nil
   then show ?case by auto
 next
   case (Cons a \<Delta>)
   then show ?case
     by (metis append_Cons append_Nil type_weaken validE(3))
 qed
 
 text \<open>A.6\<close>
 
 lemma strengthening:
   assumes "(\<Gamma> @ VarB x Q # \<Delta>) \<turnstile> S <: T"
   shows  "(\<Gamma>@\<Delta>) \<turnstile> S <: T"
   using assms
 proof (induct "\<Gamma> @ VarB x Q # \<Delta>" S T arbitrary: \<Gamma>)
   case (SA_Top S)
   then have "\<turnstile> (\<Gamma> @ \<Delta>) ok" by (auto dest: valid_cons')
   moreover have "S closed_in (\<Gamma> @ \<Delta>)" using SA_Top by (auto dest: closed_in_cons)
   ultimately show ?case using subtype_of.SA_Top by auto
 next
   case (SA_refl_TVar X)
   from \<open>\<turnstile> (\<Gamma> @ VarB x Q # \<Delta>) ok\<close>
   have h1:"\<turnstile> (\<Gamma> @ \<Delta>) ok" by (auto dest: valid_cons')
   have "X \<in> ty_dom (\<Gamma> @ VarB x Q # \<Delta>)" using SA_refl_TVar by auto
   then have h2:"X \<in> ty_dom (\<Gamma> @ \<Delta>)" using ty_dom_vrs by auto
   show ?case using h1 h2 by auto
 next
   case (SA_all T1 S1 X S2 T2)
   have h1:"((TVarB X T1 # \<Gamma>) @ \<Delta>)\<turnstile>S2<:T2" by (fastforce intro: SA_all)
   have h2:"(\<Gamma> @ \<Delta>)\<turnstile>T1<:S1" using SA_all by auto
   then show ?case using h1 h2 by auto
 qed (auto)
 
 lemma narrow_type: \<comment> \<open>A.7\<close>
   assumes H: "\<Delta> @ (TVarB X Q) # \<Gamma> \<turnstile> t : T"
   shows "\<Gamma> \<turnstile> P <: Q \<Longrightarrow> \<Delta> @ (TVarB X P) # \<Gamma> \<turnstile> t : T"
   using H
   proof (nominal_induct "\<Delta> @ (TVarB X Q) # \<Gamma>" t T avoiding: P arbitrary: \<Delta> rule: typing.strong_induct)
     case (T_Var x T P D)
     then have "VarB x T \<in> set (D @ TVarB X P # \<Gamma>)" 
       and "\<turnstile>  (D @ TVarB X P # \<Gamma>) ok"
       by (auto intro: replace_type dest!: subtype_implies_closed)
     then show ?case by auto
   next
     case (T_App t1 T1 T2 t2 P D)
     then show ?case by force
   next
     case (T_Abs x T1 t2 T2 P D)
     then show ?case by (fastforce dest: typing_ok)
   next
     case (T_Sub t S T P D)
     then show ?case using subtype_narrow by fastforce
   next
     case (T_TAbs X' T1 t2 T2 P D)
     then show ?case by (fastforce dest: typing_ok)
   next
     case (T_TApp X' t1 T2 T11 T12 P D)
     then have "D @ TVarB X P # \<Gamma> \<turnstile> t1 : Forall X' T12 T11" by fastforce
     moreover have "(D @ [TVarB X Q] @ \<Gamma>) \<turnstile> T2<:T11" using T_TApp by auto
     then have "(D @ [TVarB X P] @ \<Gamma>) \<turnstile> T2<:T11" using \<open>\<Gamma>\<turnstile>P<:Q\<close>
       by (rule subtype_narrow)
     moreover from T_TApp have "X' \<sharp> (D @ TVarB X P # \<Gamma>, t1, T2)"
       by (simp add: fresh_list_append fresh_list_cons fresh_prod)
     ultimately show ?case by auto
 qed
 
 subsection \<open>Substitution lemmas\<close>
 
 subsubsection \<open>Substition Preserves Typing\<close>
 
 theorem subst_type: \<comment> \<open>A.8\<close>
   assumes H: "(\<Delta> @ (VarB x U) # \<Gamma>) \<turnstile> t : T"
   shows "\<Gamma> \<turnstile> u : U \<Longrightarrow> \<Delta> @ \<Gamma> \<turnstile> t[x \<mapsto> u] : T" using H
  proof (nominal_induct "\<Delta> @ (VarB x U) # \<Gamma>" t T avoiding: x u arbitrary: \<Delta> rule: typing.strong_induct)
    case (T_Var y T x u D)
    show ?case
    proof (cases "x = y")
      assume eq:"x=y"
      then have "T=U" using T_Var uniqueness_of_ctxt' by auto
      then show ?case using eq T_Var
        by (auto intro: type_weaken' dest: valid_cons')
    next
      assume "x\<noteq>y"
      then show ?case using T_Var
        by (auto simp:binding.inject dest: valid_cons')
    qed
  next
    case (T_App t1 T1 T2 t2 x u D)
    then show ?case by force
  next
    case (T_Abs y T1 t2 T2 x u D)
    then show ?case by force
  next
    case (T_Sub t S T x u D)
    then have "D @ \<Gamma> \<turnstile> t[x \<mapsto> u] : S" by auto
    moreover have "(D @ \<Gamma>) \<turnstile> S<:T" using T_Sub by (auto dest: strengthening)
    ultimately show ?case by auto 
  next
    case (T_TAbs X T1 t2 T2 x u D)
    from \<open>TVarB X T1 # D @ VarB x U # \<Gamma> \<turnstile> t2 : T2\<close> have "X \<sharp> T1"
      by (auto simp: valid_ty_dom_fresh dest: typing_ok intro!: closed_in_fresh)
    with \<open>X \<sharp> u\<close> and T_TAbs show ?case by fastforce
  next
    case (T_TApp X t1 T2 T11 T12 x u D)
    then have "(D@\<Gamma>) \<turnstile>T2<:T11" using T_TApp by (auto dest: strengthening)
    then show "((D @ \<Gamma>) \<turnstile> ((t1 \<cdot>\<^sub>\<tau> T2)[x \<mapsto> u]) : (T12[X \<mapsto> T2]\<^sub>\<tau>))" using T_TApp
      by (force simp: fresh_prod fresh_list_append fresh_list_cons subst_trm_fresh_tyvar)
 qed
 
 subsubsection \<open>Type Substitution Preserves Subtyping\<close>
 
 lemma substT_subtype: \<comment> \<open>A.10\<close>
   assumes H: "(\<Delta> @ ((TVarB X Q) # \<Gamma>)) \<turnstile> S <: T"
   shows "\<Gamma> \<turnstile> P <: Q \<Longrightarrow> (\<Delta>[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<mapsto> P]\<^sub>\<tau> <: T[X \<mapsto> P]\<^sub>\<tau>" 
   using H
 proof (nominal_induct "\<Delta> @ TVarB X Q # \<Gamma>" S T avoiding: X P arbitrary: \<Delta> rule: subtype_of.strong_induct)
   case (SA_Top S X P D)
   then have "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by simp
   moreover have closed: "P closed_in \<Gamma>" using SA_Top subtype_implies_closed by auto 
   ultimately have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule valid_subst)
   moreover from SA_Top have "S closed_in (D @ TVarB X Q # \<Gamma>)" by simp
   then have "S[X \<mapsto> P]\<^sub>\<tau> closed_in  (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" using closed by (rule subst_closed_in)
   ultimately show ?case by auto
 next
   case (SA_trans_TVar Y S T X P D)
   have h:"(D @ TVarB X Q # \<Gamma>)\<turnstile>S<:T" by fact
   then have ST: "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S[X \<mapsto> P]\<^sub>\<tau> <: T[X \<mapsto> P]\<^sub>\<tau>" using SA_trans_TVar by auto
   from h have G_ok: "\<turnstile> (D @ TVarB X Q # \<Gamma>) ok" by (rule subtype_implies_ok)
   from G_ok and SA_trans_TVar have X_\<Gamma>_ok: "\<turnstile> (TVarB X Q # \<Gamma>) ok"
     by (auto intro: validE_append)
   show "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> Tvar Y[X \<mapsto> P]\<^sub>\<tau><:T[X \<mapsto> P]\<^sub>\<tau>"
   proof (cases "X = Y")
     assume eq: "X = Y"
     from eq and SA_trans_TVar have "TVarB Y Q \<in> set (D @ TVarB X Q # \<Gamma>)" by simp
     with G_ok have QS: "Q = S" using \<open>TVarB Y S \<in> set (D @ TVarB X Q # \<Gamma>)\<close>
       by (rule uniqueness_of_ctxt)
     from X_\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "Q closed_in \<Gamma>" by auto
     then have XQ: "X \<sharp> Q" by (rule closed_in_fresh)
     note \<open>\<Gamma>\<turnstile>P<:Q\<close>
     moreover from ST have "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" by (rule subtype_implies_ok)
     moreover have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) extends \<Gamma>" by (simp add: extends_def)
     ultimately have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:Q" by (rule weakening)
     with QS have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:S" by simp
     moreover from XQ and ST and QS have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> S<:T[X \<mapsto> P]\<^sub>\<tau>"
       by (simp add: type_subst_identity)
     ultimately have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>) \<turnstile> P<:T[X \<mapsto> P]\<^sub>\<tau>"
       by (rule subtype_transitivity)
     with eq show ?case by simp
   next
     assume neq: "X \<noteq> Y"
     with SA_trans_TVar have "TVarB Y S \<in> set D \<or> TVarB Y S \<in> set \<Gamma>"
       by (simp add: binding.inject)
     then show ?case
     proof
       assume "TVarB Y S \<in> set D"
       then have "TVarB Y (S[X \<mapsto> P]\<^sub>\<tau>) \<in> set (D[X \<mapsto> P]\<^sub>e)"
         by (rule ctxt_subst_mem_TVarB)
       then have "TVarB Y (S[X \<mapsto> P]\<^sub>\<tau>) \<in> set (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" by simp
       with neq and ST show ?thesis by auto
     next
       assume Y: "TVarB Y S \<in> set \<Gamma>"
       from X_\<Gamma>_ok have "X \<sharp> ty_dom \<Gamma>" and "\<turnstile> \<Gamma> ok" by auto
       then have "X \<sharp> \<Gamma>" by (simp add: valid_ty_dom_fresh)
       with Y have "X \<sharp> S"
         by (induct \<Gamma>) (auto simp: fresh_list_nil fresh_list_cons)
       with ST have "(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S<:T[X \<mapsto> P]\<^sub>\<tau>"
         by (simp add: type_subst_identity)
       moreover from Y have "TVarB Y S \<in> set (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)" by simp
       ultimately show ?thesis using neq by auto
     qed
   qed
 next
   case (SA_refl_TVar Y X P D)
   note \<open>\<turnstile> (D @ TVarB X Q # \<Gamma>) ok\<close>
   moreover from SA_refl_TVar have closed: "P closed_in \<Gamma>"
     by (auto dest: subtype_implies_closed)
   ultimately have ok: "\<turnstile> (D[X \<mapsto> P]\<^sub>e @ \<Gamma>) ok" using valid_subst by auto
   from closed have closed': "P closed_in (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)"
     by (simp add: closed_in_weaken')
   show ?case
   proof (cases "X = Y")
     assume "X = Y"
     with closed' and ok show ?thesis
       by (auto intro: subtype_reflexivity)
   next
     assume neq: "X \<noteq> Y"
     with SA_refl_TVar have "Y \<in> ty_dom (D[X \<mapsto> P]\<^sub>e @ \<Gamma>)"
       by (simp add: ty_dom_subst doms_append)
     with neq and ok show ?thesis by auto
   qed
 next
   case (SA_arrow T1 S1 S2 T2 X P D)
   then have h1:"(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>T1[X \<mapsto> P]\<^sub>\<tau><:S1[X \<mapsto> P]\<^sub>\<tau>" using SA_arrow by auto
   from SA_arrow have h2:"(D[X \<mapsto> P]\<^sub>e @ \<Gamma>)\<turnstile>S2[X \<mapsto> P]\<^sub>\<tau><:T2[X \<mapsto> P]\<^sub>\<tau>" using SA_arrow by auto
   show ?case using subtype_of.SA_arrow h1 h2 by auto
 next
   case (SA_all T1 S1 Y S2 T2 X P D)
   then have Y: "Y \<sharp> ty_dom (D @ TVarB X Q # \<Gamma>)"
     by (auto dest: subtype_implies_ok intro: fresh_dom)
   moreover from SA_all have "S1 closed_in (D @ TVarB X Q # \<Gamma>)"
     by (auto dest: subtype_implies_closed)
   ultimately have S1: "Y \<sharp> S1" by (rule closed_in_fresh)
   from SA_all have "T1 closed_in (D @ TVarB X Q # \<Gamma>)"
     by (auto dest: subtype_implies_closed)
   with Y have T1: "Y \<sharp> T1" by (rule closed_in_fresh)
   with SA_all and S1 show ?case by force
 qed
 
 subsubsection \<open>Type Substitution Preserves Typing\<close>
 
 theorem substT_type: \<comment> \<open>A.11\<close>
   assumes H: "(D @ TVarB X Q # G) \<turnstile> t : T"
   shows "G \<turnstile> P <: Q \<Longrightarrow>
     (D[X \<mapsto> P]\<^sub>e @ G) \<turnstile> t[X \<mapsto>\<^sub>\<tau> P] : T[X \<mapsto> P]\<^sub>\<tau>" using H
 proof (nominal_induct "D @ TVarB X Q # G" t T avoiding: X P arbitrary: D rule: typing.strong_induct)
   case (T_Var x T X P D')
   have "G\<turnstile>P<:Q" by fact
   then have "P closed_in G" using subtype_implies_closed by auto
   moreover note \<open>\<turnstile> (D' @ TVarB X Q # G) ok\<close>
   ultimately have "\<turnstile> (D'[X \<mapsto> P]\<^sub>e @ G) ok" using valid_subst by auto
   moreover note \<open>VarB x T \<in> set (D' @ TVarB X Q # G)\<close>
   then have "VarB x T \<in> set D' \<or> VarB x T \<in> set G" by simp
   then have "(VarB x (T[X \<mapsto> P]\<^sub>\<tau>)) \<in> set (D'[X \<mapsto> P]\<^sub>e @ G)"
   proof
     assume "VarB x T \<in> set D'"
     then have "VarB x (T[X \<mapsto> P]\<^sub>\<tau>) \<in> set (D'[X \<mapsto> P]\<^sub>e)"
       by (rule ctxt_subst_mem_VarB)
     then show ?thesis by simp
   next
     assume x: "VarB x T \<in> set G"
     from T_Var have ok: "\<turnstile> G ok" by (auto dest: subtype_implies_ok)
     then have "X \<sharp> ty_dom G" using T_Var by (auto dest: validE_append)
     with ok have "X \<sharp> G" by (simp add: valid_ty_dom_fresh)
     moreover from x have "VarB x T \<in> set (D' @ G)" by simp
     then have "VarB x (T[X \<mapsto> P]\<^sub>\<tau>) \<in> set ((D' @ G)[X \<mapsto> P]\<^sub>e)"
       by (rule ctxt_subst_mem_VarB)
     ultimately show ?thesis
       by (simp add: ctxt_subst_append ctxt_subst_identity)
   qed
   ultimately show ?case by auto
 next
   case (T_App t1 T1 T2 t2 X P D')
   then have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t1[X \<mapsto>\<^sub>\<tau> P] : (T1 \<rightarrow> T2)[X \<mapsto> P]\<^sub>\<tau>" by auto
   moreover from T_App have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t2[X \<mapsto>\<^sub>\<tau> P] : T1[X \<mapsto> P]\<^sub>\<tau>" by auto
   ultimately show ?case by auto
 next
   case (T_Abs x T1 t2 T2 X P D')
   then show ?case by force
 next
   case (T_Sub t S T X P D')
   then show ?case using substT_subtype by force
 next
   case (T_TAbs X' T1 t2 T2 X P D')
   then have "X' \<sharp> ty_dom (D' @ TVarB X Q # G)"
   and "T1 closed_in (D' @ TVarB X Q # G)"
     by (auto dest: typing_ok)
   then have "X' \<sharp> T1" by (rule closed_in_fresh)
   with T_TAbs show ?case by force
 next
   case (T_TApp X' t1 T2 T11 T12 X P D')
   then have "X' \<sharp> ty_dom (D' @ TVarB X Q # G)"
     by (simp add: fresh_dom)
   moreover from T_TApp have "T11 closed_in (D' @ TVarB X Q # G)"
     by (auto dest: subtype_implies_closed)
   ultimately have X': "X' \<sharp> T11" by (rule closed_in_fresh)
   from T_TApp have "D'[X \<mapsto> P]\<^sub>e @ G \<turnstile> t1[X \<mapsto>\<^sub>\<tau> P] : (\<forall>X'<:T11. T12)[X \<mapsto> P]\<^sub>\<tau>"
     by simp
   with X' and T_TApp show ?case
     by (auto simp: fresh_atm type_substitution_lemma
       fresh_list_append fresh_list_cons
       ctxt_subst_fresh' type_subst_fresh subst_trm_ty_fresh
       intro: substT_subtype)
 qed
 
 lemma Abs_type: \<comment> \<open>A.13(1)\<close>
   assumes H: "\<Gamma> \<turnstile> (\<lambda>x:S. s) : T"
   and H': "\<Gamma> \<turnstile> T <: U \<rightarrow> U'"
   and H'': "x \<sharp> \<Gamma>"
   obtains S' where "\<Gamma> \<turnstile> U <: S"
              and   "(VarB x S) # \<Gamma> \<turnstile> s : S'"
              and   "\<Gamma> \<turnstile> S' <: U'"
   using H H' H''
 proof (nominal_induct \<Gamma> t \<equiv> "\<lambda>x:S. s" T avoiding: x arbitrary: U U' S s rule: typing.strong_induct)
   case (T_Abs y T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2)
   from \<open>\<Gamma> \<turnstile> T\<^sub>1 \<rightarrow> T\<^sub>2 <: U \<rightarrow> U'\<close>
   obtain ty1: "\<Gamma> \<turnstile> U <: S" and ty2: "\<Gamma> \<turnstile> T\<^sub>2 <: U'" using T_Abs
     by cases (simp_all add: ty.inject trm.inject alpha fresh_atm)
   from T_Abs have "VarB y S # \<Gamma> \<turnstile> [(y, x)] \<bullet> s : T\<^sub>2"
     by (simp add: trm.inject alpha fresh_atm)
   then have "[(y, x)] \<bullet> (VarB y S # \<Gamma>) \<turnstile> [(y, x)] \<bullet> [(y, x)] \<bullet> s : [(y, x)] \<bullet> T\<^sub>2"
     by (rule typing.eqvt)
   moreover from T_Abs have "y \<sharp> \<Gamma>"
     by (auto dest!: typing_ok simp add: fresh_trm_dom)
   ultimately have "VarB x S # \<Gamma> \<turnstile> s : T\<^sub>2" using T_Abs
     by (perm_simp add: ty_vrs_prm_simp)
   with ty1 show ?case using ty2 by (rule T_Abs)
 next
   case (T_Sub \<Gamma> t S T)
   then show ?case using subtype_transitivity by blast
 qed simp_all
 
 lemma subtype_reflexivity_from_typing:
   assumes "\<Gamma> \<turnstile> t : T"
   shows "\<Gamma> \<turnstile> T <: T"
 using assms subtype_reflexivity typing_ok typing_closed_in by simp
 
 lemma Abs_type':
   assumes H: "\<Gamma> \<turnstile> (\<lambda>x:S. s) : U \<rightarrow> U'"
   and H': "x \<sharp> \<Gamma>"
   obtains S'
   where "\<Gamma> \<turnstile> U <: S"
   and "(VarB x S) # \<Gamma> \<turnstile> s : S'"
   and "\<Gamma> \<turnstile> S' <: U'"
   using H subtype_reflexivity_from_typing [OF H] H'
   by (rule Abs_type)
 
 lemma TAbs_type: \<comment> \<open>A.13(2)\<close>
   assumes H: "\<Gamma> \<turnstile> (\<lambda>X<:S. s) : T"
   and H': "\<Gamma> \<turnstile> T <: (\<forall>X<:U. U')"
   and fresh: "X \<sharp> \<Gamma>" "X \<sharp> S" "X \<sharp> U"
   obtains S'
   where "\<Gamma> \<turnstile> U <: S"
   and   "(TVarB X U # \<Gamma>) \<turnstile> s : S'"
   and   "(TVarB X U # \<Gamma>) \<turnstile> S' <: U'"
   using H H' fresh
 proof (nominal_induct \<Gamma> t \<equiv> "\<lambda>X<:S. s" T avoiding: X U U' S arbitrary: s rule: typing.strong_induct)
   case (T_TAbs Y T\<^sub>1 \<Gamma> t\<^sub>2 T\<^sub>2)
   from \<open>TVarB Y T\<^sub>1 # \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2\<close> have Y: "Y \<sharp> \<Gamma>"
     by (auto dest!: typing_ok simp add: valid_ty_dom_fresh)
   from \<open>Y \<sharp> U'\<close> and \<open>Y \<sharp> X\<close>
   have "(\<forall>X<:U. U') = (\<forall>Y<:U. [(Y, X)] \<bullet> U')"
     by (simp add: ty.inject alpha' fresh_atm)
   with T_TAbs have "\<Gamma> \<turnstile> (\<forall>Y<:S. T\<^sub>2) <: (\<forall>Y<:U. [(Y, X)] \<bullet> U')" by (simp add: trm.inject)
   then obtain ty1: "\<Gamma> \<turnstile> U <: S" and ty2: "(TVarB Y U # \<Gamma>) \<turnstile> T\<^sub>2 <: ([(Y, X)] \<bullet> U')" using T_TAbs Y
     by (cases rule: subtype_of.strong_cases [where X=Y]) (simp_all add: ty.inject alpha abs_fresh)
   note ty1
   moreover from T_TAbs have "TVarB Y S # \<Gamma> \<turnstile> ([(Y, X)] \<bullet> s) : T\<^sub>2"
     by (simp add: trm.inject alpha fresh_atm)
   then have "[(Y, X)] \<bullet> (TVarB Y S # \<Gamma>) \<turnstile> [(Y, X)] \<bullet> [(Y, X)] \<bullet> s : [(Y, X)] \<bullet> T\<^sub>2"
     by (rule typing.eqvt)
   with \<open>X \<sharp> \<Gamma>\<close> \<open>X \<sharp> S\<close> Y \<open>Y \<sharp> S\<close> have "TVarB X S # \<Gamma> \<turnstile> s : [(Y, X)] \<bullet> T\<^sub>2"
     by perm_simp
   then have "TVarB X U # \<Gamma> \<turnstile> s : [(Y, X)] \<bullet> T\<^sub>2" using ty1
     by (rule narrow_type [of "[]", simplified])
   moreover from ty2 have "([(Y, X)] \<bullet> (TVarB Y U # \<Gamma>)) \<turnstile> ([(Y, X)] \<bullet> T\<^sub>2) <: ([(Y, X)] \<bullet> [(Y, X)] \<bullet> U')"
     by (rule subtype_of.eqvt)
   with \<open>X \<sharp> \<Gamma>\<close> \<open>X \<sharp> U\<close> Y \<open>Y \<sharp> U\<close> have "(TVarB X U # \<Gamma>) \<turnstile> ([(Y, X)] \<bullet> T\<^sub>2) <: U'"
     by perm_simp
   ultimately show ?case by (rule T_TAbs)
 next
   case (T_Sub \<Gamma> t S T)
   then show ?case using subtype_transitivity by blast 
 qed simp_all
 
 lemma TAbs_type':
   assumes H: "\<Gamma> \<turnstile> (\<lambda>X<:S. s) : (\<forall>X<:U. U')"
   and fresh: "X \<sharp> \<Gamma>" "X \<sharp> S" "X \<sharp> U"
   obtains S'
   where "\<Gamma> \<turnstile> U <: S"
   and "(TVarB X U # \<Gamma>) \<turnstile> s : S'"
   and "(TVarB X U # \<Gamma>) \<turnstile> S' <: U'"
   using H subtype_reflexivity_from_typing [OF H] fresh
   by (rule TAbs_type)
 
 theorem preservation: \<comment> \<open>A.20\<close>
   assumes H: "\<Gamma> \<turnstile> t : T"
   shows "t \<longmapsto> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : T" using H
 proof (nominal_induct avoiding: t' rule: typing.strong_induct)
   case (T_App \<Gamma> t\<^sub>1 T\<^sub>11 T\<^sub>12 t\<^sub>2 t')
   obtain x::vrs where x_fresh: "x \<sharp> (\<Gamma>, t\<^sub>1 \<cdot> t\<^sub>2, t')"
     by (rule exists_fresh) (rule fin_supp)
   obtain X::tyvrs where "X \<sharp> (t\<^sub>1 \<cdot> t\<^sub>2, t')"
     by (rule exists_fresh) (rule fin_supp)
   with \<open>t\<^sub>1 \<cdot> t\<^sub>2 \<longmapsto> t'\<close> show ?case
   proof (cases rule: eval.strong_cases [where x=x and X=X])
     case (E_Abs v\<^sub>2 T\<^sub>11' t\<^sub>12)
     with T_App and x_fresh have h: "\<Gamma> \<turnstile> (\<lambda>x:T\<^sub>11'. t\<^sub>12) : T\<^sub>11 \<rightarrow> T\<^sub>12"
       by (simp add: trm.inject fresh_prod)
     moreover from x_fresh have "x \<sharp> \<Gamma>" by simp
     ultimately obtain S'
       where T\<^sub>11: "\<Gamma> \<turnstile> T\<^sub>11 <: T\<^sub>11'"
       and t\<^sub>12: "(VarB x T\<^sub>11') # \<Gamma> \<turnstile> t\<^sub>12 : S'"
       and S': "\<Gamma> \<turnstile> S' <: T\<^sub>12"
       by (rule Abs_type') blast
     from \<open>\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11\<close>
     have "\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11'" using T\<^sub>11 by (rule T_Sub)
     with t\<^sub>12 have "\<Gamma> \<turnstile> t\<^sub>12[x \<mapsto> t\<^sub>2] : S'" 
       by (rule subst_type [where \<Delta>="[]", simplified])
     hence "\<Gamma> \<turnstile> t\<^sub>12[x \<mapsto> t\<^sub>2] : T\<^sub>12" using S' by (rule T_Sub)
     with E_Abs and x_fresh show ?thesis by (simp add: trm.inject fresh_prod)
   next
     case (E_App1 t''' t'' u)
     hence "t\<^sub>1 \<longmapsto> t''" by (simp add:trm.inject) 
     hence "\<Gamma> \<turnstile> t'' : T\<^sub>11 \<rightarrow> T\<^sub>12" by (rule T_App)
     hence "\<Gamma> \<turnstile> t'' \<cdot> t\<^sub>2 : T\<^sub>12" using \<open>\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>11\<close>
       by (rule typing.T_App)
     with E_App1 show ?thesis by (simp add:trm.inject)
   next
     case (E_App2 v t''' t'')
     hence "t\<^sub>2 \<longmapsto> t''" by (simp add:trm.inject) 
     hence "\<Gamma> \<turnstile> t'' : T\<^sub>11" by (rule T_App)
     with T_App(1) have "\<Gamma> \<turnstile> t\<^sub>1 \<cdot> t'' : T\<^sub>12"
       by (rule typing.T_App)
     with E_App2 show ?thesis by (simp add:trm.inject) 
   qed (simp_all add: fresh_prod)
 next
   case (T_TApp X \<Gamma> t\<^sub>1 T\<^sub>2  T\<^sub>11  T\<^sub>12 t')
   obtain x::vrs where "x \<sharp> (t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2, t')"
     by (rule exists_fresh) (rule fin_supp)
   with \<open>t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2 \<longmapsto> t'\<close>
   show ?case
   proof (cases rule: eval.strong_cases [where X=X and x=x])
     case (E_TAbs T\<^sub>11' T\<^sub>2' t\<^sub>12)
     with T_TApp have "\<Gamma> \<turnstile> (\<lambda>X<:T\<^sub>11'. t\<^sub>12) : (\<forall>X<:T\<^sub>11. T\<^sub>12)" and "X \<sharp> \<Gamma>" and "X \<sharp> T\<^sub>11'"
       by (simp_all add: trm.inject)
     moreover from \<open>\<Gamma>\<turnstile>T\<^sub>2<:T\<^sub>11\<close> and \<open>X \<sharp> \<Gamma>\<close> have "X \<sharp> T\<^sub>11"
       by (blast intro: closed_in_fresh fresh_dom dest: subtype_implies_closed)
     ultimately obtain S'
       where "TVarB X T\<^sub>11 # \<Gamma> \<turnstile> t\<^sub>12 : S'"
       and "(TVarB X T\<^sub>11 # \<Gamma>) \<turnstile> S' <: T\<^sub>12"
       by (rule TAbs_type') blast
     hence "TVarB X T\<^sub>11 # \<Gamma> \<turnstile> t\<^sub>12 : T\<^sub>12" by (rule T_Sub)
     hence "\<Gamma> \<turnstile> t\<^sub>12[X \<mapsto>\<^sub>\<tau> T\<^sub>2] : T\<^sub>12[X \<mapsto> T\<^sub>2]\<^sub>\<tau>" using \<open>\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<close>
       by (rule substT_type [where D="[]", simplified])
     with T_TApp and E_TAbs show ?thesis by (simp add: trm.inject)
   next
     case (E_TApp t''' t'' T)
     from E_TApp have "t\<^sub>1 \<longmapsto> t''" by (simp add: trm.inject)
     then have "\<Gamma> \<turnstile> t'' : (\<forall>X<:T\<^sub>11. T\<^sub>12)" by (rule T_TApp)
     then have "\<Gamma> \<turnstile> t'' \<cdot>\<^sub>\<tau> T\<^sub>2 : T\<^sub>12[X \<mapsto> T\<^sub>2]\<^sub>\<tau>" using \<open>\<Gamma> \<turnstile> T\<^sub>2 <: T\<^sub>11\<close>
       by (rule better_T_TApp)
     with E_TApp show ?thesis by (simp add: trm.inject)
   qed (simp_all add: fresh_prod)
 next
   case (T_Sub \<Gamma> t S T t')
   have "t \<longmapsto> t'" by fact
   hence "\<Gamma> \<turnstile> t' : S" by (rule T_Sub)
   moreover have "\<Gamma> \<turnstile> S <: T" by fact
   ultimately show ?case by (rule typing.T_Sub)
 qed (auto)
 
 lemma Fun_canonical: \<comment> \<open>A.14(1)\<close>
   assumes ty: "[] \<turnstile> v : T\<^sub>1 \<rightarrow> T\<^sub>2"
   shows "val v \<Longrightarrow> \<exists>x t S. v = (\<lambda>x:S. t)" using ty
 proof (induct "[]::env" v "T\<^sub>1 \<rightarrow> T\<^sub>2" arbitrary: T\<^sub>1 T\<^sub>2)
   case (T_Sub t S)
   from \<open>[] \<turnstile> S <: T\<^sub>1 \<rightarrow> T\<^sub>2\<close>
   obtain S\<^sub>1 S\<^sub>2 where S: "S = S\<^sub>1 \<rightarrow> S\<^sub>2" 
     by cases (auto simp: T_Sub)
   then show ?case using \<open>val t\<close> by (rule T_Sub)
 qed (auto)
 
 lemma TyAll_canonical: \<comment> \<open>A.14(3)\<close>
   fixes X::tyvrs
   assumes ty: "[] \<turnstile> v : (\<forall>X<:T\<^sub>1. T\<^sub>2)"
   shows "val v \<Longrightarrow> \<exists>X t S. v = (\<lambda>X<:S. t)" using ty
 proof (induct "[]::env" v "\<forall>X<:T\<^sub>1. T\<^sub>2" arbitrary: X T\<^sub>1 T\<^sub>2)
   case (T_Sub t S)
   from \<open>[] \<turnstile> S <: (\<forall>X<:T\<^sub>1. T\<^sub>2)\<close>
   obtain X S\<^sub>1 S\<^sub>2 where S: "S = (\<forall>X<:S\<^sub>1. S\<^sub>2)"
     by cases (auto simp: T_Sub)
   then show ?case using T_Sub by auto 
 qed (auto)
 
 theorem progress:
   assumes "[] \<turnstile> t : T"
   shows "val t \<or> (\<exists>t'. t \<longmapsto> t')" 
 using assms
 proof (induct "[]::env" t T)
   case (T_App t\<^sub>1 T\<^sub>11  T\<^sub>12 t\<^sub>2)
   hence "val t\<^sub>1 \<or> (\<exists>t'. t\<^sub>1 \<longmapsto> t')" by simp
   thus ?case
   proof
     assume t\<^sub>1_val: "val t\<^sub>1"
     with T_App obtain x t3 S where t\<^sub>1: "t\<^sub>1 = (\<lambda>x:S. t3)"
       by (auto dest!: Fun_canonical)
     from T_App have "val t\<^sub>2 \<or> (\<exists>t'. t\<^sub>2 \<longmapsto> t')" by simp
     thus ?case
     proof
       assume "val t\<^sub>2"
       with t\<^sub>1 have "t\<^sub>1 \<cdot> t\<^sub>2 \<longmapsto> t3[x \<mapsto> t\<^sub>2]" by auto
       thus ?case by auto
     next
       assume "\<exists>t'. t\<^sub>2 \<longmapsto> t'"
       then obtain t' where "t\<^sub>2 \<longmapsto> t'" by auto
       with t\<^sub>1_val have "t\<^sub>1 \<cdot> t\<^sub>2 \<longmapsto> t\<^sub>1 \<cdot> t'" by auto
       thus ?case by auto
     qed
   next
     assume "\<exists>t'. t\<^sub>1 \<longmapsto> t'"
     then obtain t' where "t\<^sub>1 \<longmapsto> t'" by auto
     hence "t\<^sub>1 \<cdot> t\<^sub>2 \<longmapsto> t' \<cdot> t\<^sub>2" by auto
     thus ?case by auto
   qed
 next
   case (T_TApp X t\<^sub>1 T\<^sub>2 T\<^sub>11 T\<^sub>12)
   hence "val t\<^sub>1 \<or> (\<exists>t'. t\<^sub>1 \<longmapsto> t')" by simp
   thus ?case
   proof
     assume "val t\<^sub>1"
     with T_TApp obtain x t S where "t\<^sub>1 = (\<lambda>x<:S. t)"
       by (auto dest!: TyAll_canonical)
     hence "t\<^sub>1 \<cdot>\<^sub>\<tau> T\<^sub>2 \<longmapsto> t[x \<mapsto>\<^sub>\<tau> T\<^sub>2]" by auto
     thus ?case by auto
   next
     assume "\<exists>t'. t\<^sub>1 \<longmapsto> t'" thus ?case by auto
   qed
 qed (auto)
 
 end
diff --git a/src/HOL/Nominal/Examples/Lam_Funs.thy b/src/HOL/Nominal/Examples/Lam_Funs.thy
--- a/src/HOL/Nominal/Examples/Lam_Funs.thy
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy
@@ -1,152 +1,149 @@
 theory Lam_Funs
   imports "HOL-Nominal.Nominal"
 begin
 
 text \<open>
   Provides useful definitions for reasoning
   with lambda-terms. 
 \<close>
 
 atom_decl name
 
 nominal_datatype lam = 
     Var "name"
   | App "lam" "lam"
   | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
 text \<open>The depth of a lambda-term.\<close>
 
 nominal_primrec
   depth :: "lam \<Rightarrow> nat"
 where
   "depth (Var x) = 1"
 | "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
 | "depth (Lam [a].t) = (depth t) + 1"
-  apply(finite_guess)+
-  apply(rule TrueI)+
-  apply(simp add: fresh_nat)
-  apply(fresh_guess)+
-  done
+  by(finite_guess | simp | fresh_guess)+
 
 text \<open>
   The free variables of a lambda-term. A complication in this
   function arises from the fact that it returns a name set, which 
   is not a finitely supported type. Therefore we have to prove 
   the invariant that frees always returns a finite set of names. 
 \<close>
 
 nominal_primrec (invariant: "\<lambda>s::name set. finite s")
   frees :: "lam \<Rightarrow> name set"
 where
   "frees (Var a) = {a}"
 | "frees (App t1 t2) = (frees t1) \<union> (frees t2)"
 | "frees (Lam [a].t) = (frees t) - {a}"
-apply(finite_guess)+
-apply(simp)+ 
-apply(simp add: fresh_def)
-apply(simp add: supp_of_fin_sets[OF pt_name_inst, OF at_name_inst, OF fs_at_inst[OF at_name_inst]])
-apply(simp add: supp_atm)
-apply(blast)
+apply(finite_guess | simp add: fresh_def | fresh_guess)+
+  apply (simp add: at_fin_set_supp at_name_inst)
 apply(fresh_guess)+
 done
 
 text \<open>
   We can avoid the definition of frees by
   using the build in notion of support.
 \<close>
 
 lemma frees_equals_support:
   shows "frees t = supp t"
 by (nominal_induct t rule: lam.strong_induct)
    (simp_all add: lam.supp supp_atm abs_supp)
 
 text \<open>Parallel and single capture-avoiding substitution.\<close>
 
 fun
   lookup :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam"   
 where
   "lookup [] x        = Var x"
 | "lookup ((y,e)#\<theta>) x = (if x=y then e else lookup \<theta> x)"
 
 lemma lookup_eqvt[eqvt]:
   fixes pi::"name prm"
   and   \<theta>::"(name\<times>lam) list"
   and   X::"name"
   shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
 by (induct \<theta>) (auto simp add: eqvts)
  
 nominal_primrec
   psubst :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam"  ("_<_>" [95,95] 105)
 where
   "\<theta><(Var x)> = (lookup \<theta> x)"
 | "\<theta><(App e\<^sub>1 e\<^sub>2)> = App (\<theta><e\<^sub>1>) (\<theta><e\<^sub>2>)"
 | "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
-apply(finite_guess)+
-apply(rule TrueI)+
-apply(simp add: abs_fresh)+
-apply(fresh_guess)+
-done
+  by (finite_guess | simp add: abs_fresh | fresh_guess)+
 
 lemma psubst_eqvt[eqvt]:
   fixes pi::"name prm" 
   and   t::"lam"
   shows "pi\<bullet>(\<theta><t>) = (pi\<bullet>\<theta>)<(pi\<bullet>t)>"
 by (nominal_induct t avoiding: \<theta> rule: lam.strong_induct)
    (simp_all add: eqvts fresh_bij)
 
 abbreviation 
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100)
 where 
   "t[x::=t']  \<equiv> ([(x,t')])<t>" 
 
 lemma subst[simp]:
   shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
   and   "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
   and   "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
 by (simp_all add: fresh_list_cons fresh_list_nil)
 
 lemma subst_supp: 
   shows "supp(t1[a::=t2]) \<subseteq> (((supp(t1)-{a})\<union>supp(t2))::name set)"
-apply(nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
-apply(auto simp add: lam.supp supp_atm fresh_prod abs_supp)
-apply(blast)+
-done
+proof (nominal_induct t1 avoiding: a t2 rule: lam.strong_induct)
+  case (Var name)
+  then show ?case
+    by (simp add: lam.supp(1) supp_atm)
+next
+  case (App lam1 lam2)
+  then show ?case
+    using lam.supp(2) by fastforce
+next
+  case (Lam name lam)
+  then show ?case
+    using frees.simps(3) frees_equals_support by auto
+qed
 
 text \<open>
   Contexts - lambda-terms with a single hole.
   Note that the lambda case in contexts does not bind a 
   name, even if we introduce the notation [_]._ for CLam.
 \<close>
 nominal_datatype clam = 
     Hole ("\<box>" 1000)  
   | CAppL "clam" "lam"
   | CAppR "lam" "clam" 
   | CLam "name" "clam"  ("CLam [_]._" [100,100] 100) 
 
 text \<open>Filling a lambda-term into a context.\<close>
 
 nominal_primrec
   filling :: "clam \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100)
 where
   "\<box>\<lbrakk>t\<rbrakk> = t"
 | "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
 | "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
 | "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 
 by (rule TrueI)+
 
 text \<open>Composition od two contexts\<close>
 
 nominal_primrec
  clam_compose :: "clam \<Rightarrow> clam \<Rightarrow> clam" ("_ \<circ> _" [100,100] 100)
 where
   "\<box> \<circ> E' = E'"
 | "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
 | "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')"
 | "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')"
 by (rule TrueI)+
   
 lemma clam_compose:
   shows "(E1 \<circ> E2)\<lbrakk>t\<rbrakk> = E1\<lbrakk>E2\<lbrakk>t\<rbrakk>\<rbrakk>"
 by (induct E1 rule: clam.induct) (auto)
 
 end
diff --git a/src/HOL/Nominal/Examples/W.thy b/src/HOL/Nominal/Examples/W.thy
--- a/src/HOL/Nominal/Examples/W.thy
+++ b/src/HOL/Nominal/Examples/W.thy
@@ -1,632 +1,632 @@
 theory W
 imports "HOL-Nominal.Nominal"
 begin
 
 text \<open>Example for strong induction rules avoiding sets of atoms.\<close>
 
 atom_decl tvar var 
 
 abbreviation
   "difference_list" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" ("_ - _" [60,60] 60) 
 where
   "xs - ys \<equiv> [x \<leftarrow> xs. x\<notin>set ys]"
 
 lemma difference_eqvt_tvar[eqvt]:
   fixes pi::"tvar prm"
     and   Xs Ys::"tvar list"
   shows "pi\<bullet>(Xs - Ys) = (pi\<bullet>Xs) - (pi\<bullet>Ys)"
   by (induct Xs) (simp_all add: eqvts)
 
 lemma difference_fresh [simp]:
   fixes X::"tvar"
     and   Xs Ys::"tvar list"
   shows "X\<sharp>(Xs - Ys) \<longleftrightarrow> X\<sharp>Xs \<or> X\<in>set Ys"
   by (induct Xs) (auto simp add: fresh_list_nil fresh_list_cons fresh_atm)
 
 lemma difference_supset:
   fixes xs::"'a list"
   and   ys::"'a list"
   and   zs::"'a list"
   assumes asm: "set xs \<subseteq> set ys"
   shows "xs - ys = []"
 using asm
 by (induct xs) (auto)
 
 nominal_datatype ty = 
     TVar "tvar"
   | Fun "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
 
 nominal_datatype tyS = 
     Ty  "ty"
   | ALL "\<guillemotleft>tvar\<guillemotright>tyS" ("\<forall>[_]._" [100,100] 100)
 
 nominal_datatype trm = 
     Var "var"
   | App "trm" "trm" 
   | Lam "\<guillemotleft>var\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
   | Let "\<guillemotleft>var\<guillemotright>trm" "trm"
 
 abbreviation
   LetBe :: "var \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" ("Let _ be _ in _" [100,100,100] 100)
 where
  "Let x be t1 in t2 \<equiv> trm.Let x t2 t1"
 
 type_synonym 
   Ctxt  = "(var\<times>tyS) list" 
 
 text \<open>free type variables\<close>
 
 consts ftv :: "'a \<Rightarrow> tvar list"
 
 overloading 
   ftv_prod \<equiv> "ftv :: ('a \<times> 'b) \<Rightarrow> tvar list"
   ftv_tvar \<equiv> "ftv :: tvar \<Rightarrow> tvar list"
   ftv_var  \<equiv> "ftv :: var \<Rightarrow> tvar list"
   ftv_list \<equiv> "ftv :: 'a list \<Rightarrow> tvar list"
   ftv_ty   \<equiv> "ftv :: ty \<Rightarrow> tvar list"
 begin
 
 primrec 
   ftv_prod
 where
  "ftv_prod (x, y) = (ftv x) @ (ftv y)"
 
 definition
   ftv_tvar :: "tvar \<Rightarrow> tvar list"
 where
 [simp]: "ftv_tvar X \<equiv> [(X::tvar)]"
 
 definition
   ftv_var :: "var \<Rightarrow> tvar list"
 where
 [simp]: "ftv_var x \<equiv> []"
 
 primrec 
   ftv_list
 where
   "ftv_list [] = []"
 | "ftv_list (x#xs) = (ftv x)@(ftv_list xs)"
 
 nominal_primrec 
   ftv_ty :: "ty \<Rightarrow> tvar list"
 where
   "ftv_ty (TVar X) = [X]"
 | "ftv_ty (T1 \<rightarrow>T2) = (ftv_ty T1) @ (ftv_ty T2)"
 by (rule TrueI)+
 
 end
 
 lemma ftv_ty_eqvt[eqvt]:
   fixes pi::"tvar prm"
   and   T::"ty"
   shows "pi\<bullet>(ftv T) = ftv (pi\<bullet>T)"
 by (nominal_induct T rule: ty.strong_induct)
    (perm_simp add: append_eqvt)+
 
 overloading 
   ftv_tyS  \<equiv> "ftv :: tyS \<Rightarrow> tvar list"
 begin
 
 nominal_primrec 
   ftv_tyS :: "tyS \<Rightarrow> tvar list"
 where
   "ftv_tyS (Ty T)    = ((ftv (T::ty))::tvar list)"
 | "ftv_tyS (\<forall>[X].S) = (ftv_tyS S) - [X]"
 apply(finite_guess add: ftv_ty_eqvt fs_tvar1 | rule TrueI)+
   apply (metis difference_fresh list.set_intros(1))
 apply(fresh_guess add: ftv_ty_eqvt fs_tvar1)+
 done
 
 end
 
 lemma ftv_tyS_eqvt[eqvt]:
   fixes pi::"tvar prm"
   and   S::"tyS"
   shows "pi\<bullet>(ftv S) = ftv (pi\<bullet>S)"
 proof (nominal_induct S rule: tyS.strong_induct)
   case (Ty ty)
   then show ?case
     by (simp add: ftv_ty_eqvt)
 next
   case (ALL tvar tyS)
   then show ?case 
     by (metis difference_eqvt_tvar ftv_ty.simps(1) ftv_tyS.simps(2) ftv_ty_eqvt ty.perm(3) tyS.perm(4))
 qed
 
 lemma ftv_Ctxt_eqvt[eqvt]:
   fixes pi::"tvar prm"
     and   \<Gamma>::"Ctxt"
   shows "pi\<bullet>(ftv \<Gamma>) = ftv (pi\<bullet>\<Gamma>)"
   by (induct \<Gamma>) (auto simp add: eqvts)
 
 text \<open>Valid\<close>
 inductive
   valid :: "Ctxt \<Rightarrow> bool"
 where
   V_Nil[intro]:  "valid []"
 | V_Cons[intro]: "\<lbrakk>valid \<Gamma>;x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((x,S)#\<Gamma>)"
 
 equivariance valid
 
 text \<open>General\<close>
 primrec gen :: "ty \<Rightarrow> tvar list \<Rightarrow> tyS" where
   "gen T [] = Ty T"
 | "gen T (X#Xs) = \<forall>[X].(gen T Xs)"
 
 lemma gen_eqvt[eqvt]:
   fixes pi::"tvar prm"
   shows "pi\<bullet>(gen T Xs) = gen (pi\<bullet>T) (pi\<bullet>Xs)"
   by (induct Xs) (simp_all add: eqvts)
 
 
 
 abbreviation 
   close :: "Ctxt \<Rightarrow> ty \<Rightarrow> tyS"
 where 
   "close \<Gamma> T \<equiv> gen T ((ftv T) - (ftv \<Gamma>))"
 
 lemma close_eqvt[eqvt]:
   fixes pi::"tvar prm"
   shows "pi\<bullet>(close \<Gamma> T) = close (pi\<bullet>\<Gamma>) (pi\<bullet>T)"
   by (simp_all only: eqvts)
   
 text \<open>Substitution\<close>
 
 type_synonym Subst = "(tvar\<times>ty) list"
 
 consts
   psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a"       ("_<_>" [100,60] 120)
 
 abbreviation 
   subst :: "'a \<Rightarrow> tvar \<Rightarrow> ty \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
 where
   "smth[X::=T] \<equiv> ([(X,T)])<smth>" 
 
 fun lookup :: "Subst \<Rightarrow> tvar \<Rightarrow> ty"   
 where
   "lookup [] X        = TVar X"
 | "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)"
 
 lemma lookup_eqvt[eqvt]:
   fixes pi::"tvar prm"
   shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
   by (induct \<theta>) (auto simp add: eqvts)
 
 lemma lookup_fresh:
   fixes X::"tvar"
   assumes a: "X\<sharp>\<theta>"
   shows "lookup \<theta> X = TVar X"
   using a
   by (induct \<theta>)
     (auto simp add: fresh_list_cons fresh_prod fresh_atm)
 
 overloading 
   psubst_ty \<equiv> "psubst :: Subst \<Rightarrow> ty \<Rightarrow> ty"
 begin
 
 nominal_primrec 
   psubst_ty
 where
   "\<theta><TVar X>   = lookup \<theta> X"
 | "\<theta><T\<^sub>1 \<rightarrow> T\<^sub>2> = (\<theta><T\<^sub>1>) \<rightarrow> (\<theta><T\<^sub>2>)"
 by (rule TrueI)+
 
 end
 
 lemma psubst_ty_eqvt[eqvt]:
   fixes pi::"tvar prm"
   and   \<theta>::"Subst"
   and   T::"ty"
   shows "pi\<bullet>(\<theta><T>) = (pi\<bullet>\<theta>)<(pi\<bullet>T)>"
 by (induct T rule: ty.induct) (simp_all add: eqvts)
 
 overloading 
   psubst_tyS \<equiv> "psubst :: Subst \<Rightarrow> tyS \<Rightarrow> tyS"
 begin
 
 nominal_primrec 
   psubst_tyS :: "Subst \<Rightarrow> tyS \<Rightarrow> tyS"
 where 
   "\<theta><(Ty T)> = Ty (\<theta><T>)"
 | "X\<sharp>\<theta> \<Longrightarrow> \<theta><(\<forall>[X].S)> = \<forall>[X].(\<theta><S>)"
 apply(finite_guess add: psubst_ty_eqvt fs_tvar1 | simp add: abs_fresh)+
 apply(fresh_guess add: psubst_ty_eqvt fs_tvar1)+
 done
 
 end
 
 overloading 
   psubst_Ctxt \<equiv> "psubst :: Subst \<Rightarrow> Ctxt \<Rightarrow> Ctxt"
 begin
 
 fun
   psubst_Ctxt :: "Subst \<Rightarrow> Ctxt \<Rightarrow> Ctxt"
 where
   "psubst_Ctxt \<theta> [] = []"
 | "psubst_Ctxt \<theta> ((x,S)#\<Gamma>) = (x,\<theta><S>)#(psubst_Ctxt \<theta> \<Gamma>)"
 
 end
 
 lemma fresh_lookup:
   fixes X::"tvar"
   and   \<theta>::"Subst"
   and   Y::"tvar"
   assumes asms: "X\<sharp>Y" "X\<sharp>\<theta>"
   shows "X\<sharp>(lookup \<theta> Y)"
   using asms
   by (induct \<theta>)
      (auto simp add: fresh_list_cons fresh_prod fresh_atm)
 
 lemma fresh_psubst_ty:
   fixes X::"tvar"
   and   \<theta>::"Subst"
   and   T::"ty"
   assumes asms: "X\<sharp>\<theta>" "X\<sharp>T"
   shows "X\<sharp>\<theta><T>"
   using asms
   by (nominal_induct T rule: ty.strong_induct)
      (auto simp add: fresh_list_append fresh_list_cons fresh_prod fresh_lookup)
 
 lemma fresh_psubst_tyS:
   fixes X::"tvar"
   and   \<theta>::"Subst"
   and   S::"tyS"
   assumes asms: "X\<sharp>\<theta>" "X\<sharp>S"
   shows "X\<sharp>\<theta><S>"
   using asms
   by (nominal_induct S avoiding: \<theta>  X rule: tyS.strong_induct)
      (auto simp add: fresh_psubst_ty abs_fresh)
 
 lemma fresh_psubst_Ctxt:
   fixes X::"tvar"
   and   \<theta>::"Subst"
   and   \<Gamma>::"Ctxt"
   assumes asms: "X\<sharp>\<theta>" "X\<sharp>\<Gamma>"
   shows "X\<sharp>\<theta><\<Gamma>>"
 using asms
 by (induct \<Gamma>)
    (auto simp add: fresh_psubst_tyS fresh_list_cons)
 
 lemma subst_freshfact2_ty: 
   fixes   X::"tvar"
   and     Y::"tvar"
   and     T::"ty"
   assumes asms: "X\<sharp>S"
   shows "X\<sharp>T[X::=S]"
   using asms
 by (nominal_induct T rule: ty.strong_induct)
    (auto simp add: fresh_atm)
 
 text \<open>instance of a type scheme\<close>
 inductive
   inst :: "ty \<Rightarrow> tyS \<Rightarrow> bool"("_ \<prec> _" [50,51] 50)  
 where
   I_Ty[intro]:  "T \<prec> (Ty T)" 
 | I_All[intro]: "\<lbrakk>X\<sharp>T'; T \<prec> S\<rbrakk> \<Longrightarrow> T[X::=T'] \<prec> \<forall>[X].S"
 
 equivariance inst[tvar] 
 
 nominal_inductive inst
   by (simp_all add: abs_fresh subst_freshfact2_ty)
 
 lemma subst_forget_ty:
   fixes T::"ty"
   and   X::"tvar"
   assumes a: "X\<sharp>T"
   shows "T[X::=S] = T"
   using a
   by  (nominal_induct T rule: ty.strong_induct)
       (auto simp add: fresh_atm)
 
 lemma psubst_ty_lemma:
   fixes \<theta>::"Subst"
   and   X::"tvar"
   and   T'::"ty"
   and   T::"ty"
   assumes a: "X\<sharp>\<theta>" 
   shows "\<theta><T[X::=T']> = (\<theta><T>)[X::=\<theta><T'>]"
 using a
 proof (nominal_induct T avoiding: \<theta> X T' rule: ty.strong_induct)
   case (TVar tvar)
   then show ?case
     by (simp add: fresh_atm(1) fresh_lookup lookup_fresh subst_forget_ty)
 qed auto
 
 lemma general_preserved:
   fixes \<theta>::"Subst"
   assumes a: "T \<prec> S"
   shows "\<theta><T> \<prec> \<theta><S>"
   using a
 proof (nominal_induct T S avoiding: \<theta> rule: inst.strong_induct)
   case (I_Ty T)
   then show ?case
     by (simp add: inst.I_Ty)
 next
   case (I_All X T' T S)
   then show ?case
     by (simp add: fresh_psubst_ty inst.I_All psubst_ty_lemma)
 qed
 
 
 text\<open>typing judgements\<close>
 inductive
   typing :: "Ctxt \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 
 where
   T_VAR[intro]: "\<lbrakk>valid \<Gamma>; (x,S)\<in>set \<Gamma>; T \<prec> S\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
 | T_APP[intro]: "\<lbrakk>\<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>1\<rightarrow>T\<^sub>2; \<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t\<^sub>1 t\<^sub>2 : T\<^sub>2" 
 | T_LAM[intro]: "\<lbrakk>x\<sharp>\<Gamma>;((x,Ty T\<^sub>1)#\<Gamma>) \<turnstile> t : T\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^sub>1\<rightarrow>T\<^sub>2"
 | T_LET[intro]: "\<lbrakk>x\<sharp>\<Gamma>; \<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>1; ((x,close \<Gamma> T\<^sub>1)#\<Gamma>) \<turnstile> t\<^sub>2 : T\<^sub>2; set (ftv T\<^sub>1 - ftv \<Gamma>) \<sharp>* T\<^sub>2\<rbrakk> 
                  \<Longrightarrow> \<Gamma> \<turnstile> Let x be t\<^sub>1 in t\<^sub>2 : T\<^sub>2"
 
 equivariance typing[tvar]
 
 lemma fresh_tvar_trm: 
   fixes X::"tvar"
   and   t::"trm"
   shows "X\<sharp>t"
 by (nominal_induct t rule: trm.strong_induct) 
    (simp_all add: fresh_atm abs_fresh)
 
 lemma ftv_ty: 
   fixes T::"ty"
   shows "supp T = set (ftv T)"
 by (nominal_induct T rule: ty.strong_induct) 
    (simp_all add: ty.supp supp_atm)
 
 lemma ftv_tyS: 
   fixes S::"tyS"
   shows "supp S = set (ftv S)"
 by (nominal_induct S rule: tyS.strong_induct) 
    (auto simp add: tyS.supp abs_supp ftv_ty)
 
 lemma ftv_Ctxt: 
   fixes \<Gamma>::"Ctxt"
   shows "supp \<Gamma> = set (ftv \<Gamma>)"
 proof (induct \<Gamma>)
   case Nil
   then show ?case
     by (simp add: supp_list_nil)
 next
   case (Cons c \<Gamma>)
   show ?case
   proof (cases c)
     case (Pair a b)
     with Cons show ?thesis
       by (simp add: ftv_tyS supp_atm(3) supp_list_cons supp_prod)
   qed
 qed
 
 lemma ftv_tvars:
   fixes Tvs::"tvar list"
   shows "supp Tvs = set Tvs"
   by (induct Tvs) (simp_all add: supp_list_nil supp_list_cons supp_atm)
 
 lemma difference_supp: 
   fixes xs ys::"tvar list"
   shows "((supp (xs - ys))::tvar set) = supp xs - supp ys"
   by (induct xs) (auto simp add: supp_list_nil supp_list_cons ftv_tvars)
 
 lemma set_supp_eq: 
   fixes xs::"tvar list"
   shows "set xs = supp xs"
   by (induct xs) (simp_all add: supp_list_nil supp_list_cons supp_atm)
 
 nominal_inductive2 typing
   avoids T_LET: "set (ftv T\<^sub>1 - ftv \<Gamma>)"
      apply (simp_all add: fresh_star_def fresh_def ftv_Ctxt fresh_tvar_trm)
   by (meson fresh_def fresh_tvar_trm)
 
 
 lemma perm_fresh_fresh_aux:
   "\<forall>(x,y)\<in>set (pi::tvar prm). x \<sharp> z \<and> y \<sharp> z \<Longrightarrow> pi \<bullet> (z::'a::pt_tvar) = z"
 proof (induct pi rule: rev_induct)
   case Nil
   then show ?case
     by simp
 next
   case (snoc x xs)
   then show ?case
-  apply (simp add: split_paired_all pt_tvar2)
+    unfolding split_paired_all pt_tvar2
     using perm_fresh_fresh(1) by fastforce
 qed
 
 lemma freshs_mem:
   fixes S::"tvar set"
   assumes "x \<in> S"
     and     "S \<sharp>* z"
   shows  "x \<sharp> z"
   using assms by (simp add: fresh_star_def)
 
 lemma fresh_gen_set:
   fixes X::"tvar"
   and   Xs::"tvar list"
   assumes "X\<in>set Xs" 
   shows "X\<sharp>gen T Xs"
   using assms by (induct Xs) (auto simp: abs_fresh)
 
 lemma close_fresh:
   fixes \<Gamma>::"Ctxt"
   shows "\<forall>(X::tvar)\<in>set ((ftv T) - (ftv \<Gamma>)). X\<sharp>(close \<Gamma> T)"
   by (meson fresh_gen_set)
 
 lemma gen_supp: 
   shows "(supp (gen T Xs)::tvar set) = supp T - supp Xs"
 by (induct Xs) 
    (auto simp add: supp_list_nil supp_list_cons tyS.supp abs_supp supp_atm)
 
 lemma minus_Int_eq: 
   shows "T - (T - U) = T \<inter> U"
   by blast
 
 lemma close_supp: 
   shows "supp (close \<Gamma> T) = set (ftv T) \<inter> set (ftv \<Gamma>)"
   using difference_supp ftv_ty gen_supp set_supp_eq by auto
 
 lemma better_T_LET:
   assumes x: "x\<sharp>\<Gamma>"
   and t1: "\<Gamma> \<turnstile> t\<^sub>1 : T\<^sub>1"
   and t2: "((x,close \<Gamma> T\<^sub>1)#\<Gamma>) \<turnstile> t\<^sub>2 : T\<^sub>2"
   shows "\<Gamma> \<turnstile> Let x be t\<^sub>1 in t\<^sub>2 : T\<^sub>2"
 proof -
   have fin: "finite (set (ftv T\<^sub>1 - ftv \<Gamma>))" by simp
   obtain pi where pi1: "(pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>)) \<sharp>* (T\<^sub>2, \<Gamma>)"
     and pi2: "set pi \<subseteq> set (ftv T\<^sub>1 - ftv \<Gamma>) \<times> (pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>))"
     by (rule at_set_avoiding [OF at_tvar_inst fin fs_tvar1, of "(T\<^sub>2, \<Gamma>)"])
   from pi1 have pi1': "(pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>)) \<sharp>* \<Gamma>"
     by (simp add: fresh_star_prod)
   have Gamma_fresh: "\<forall>(x,y)\<in>set pi. x \<sharp> \<Gamma> \<and> y \<sharp> \<Gamma>"
     using freshs_mem [OF _ pi1'] subsetD [OF pi2] ftv_Ctxt fresh_def by fastforce
   have "\<And>x y. \<lbrakk>x \<in> set (ftv T\<^sub>1 - ftv \<Gamma>); y \<in> pi \<bullet> set (ftv T\<^sub>1 - ftv \<Gamma>)\<rbrakk>
               \<Longrightarrow> x \<sharp> close \<Gamma> T\<^sub>1 \<and> y \<sharp> close \<Gamma> T\<^sub>1"
     by (metis DiffE filter_set fresh_def fresh_gen_set freshs_mem ftv_Ctxt ftv_ty gen_supp member_filter pi1')
   then have close_fresh': "\<forall>(x, y)\<in>set pi. x \<sharp> close \<Gamma> T\<^sub>1 \<and> y \<sharp> close \<Gamma> T\<^sub>1"
     using pi2 by auto
   note x
   moreover from Gamma_fresh perm_boolI [OF t1, of pi]
   have "\<Gamma> \<turnstile> t\<^sub>1 : pi \<bullet> T\<^sub>1"
     by (simp add: perm_fresh_fresh_aux eqvts fresh_tvar_trm)
   moreover from t2 close_fresh'
   have "(x,(pi \<bullet> close \<Gamma> T\<^sub>1))#\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2"
     by (simp add: perm_fresh_fresh_aux)
   with Gamma_fresh have "(x,close \<Gamma> (pi \<bullet> T\<^sub>1))#\<Gamma> \<turnstile> t\<^sub>2 : T\<^sub>2"
     by (simp add: close_eqvt perm_fresh_fresh_aux)
   moreover from pi1 Gamma_fresh
   have "set (ftv (pi \<bullet> T\<^sub>1) - ftv \<Gamma>) \<sharp>* T\<^sub>2"
     by (simp only: eqvts fresh_star_prod perm_fresh_fresh_aux)
   ultimately show ?thesis by (rule T_LET)
 qed
 
 lemma ftv_ty_subst:
   fixes T::"ty"
   and   \<theta>::"Subst"
   and   X Y ::"tvar"
   assumes "X \<in> set (ftv T)"
   and     "Y \<in> set (ftv (lookup \<theta> X))"
   shows "Y \<in> set (ftv (\<theta><T>))"
   using assms
   by (nominal_induct T rule: ty.strong_induct) (auto)
 
 lemma ftv_tyS_subst:
   fixes S::"tyS"
   and   \<theta>::"Subst"
   and   X Y::"tvar"
   assumes "X \<in> set (ftv S)"
   and     "Y \<in> set (ftv (lookup \<theta> X))"
   shows "Y \<in> set (ftv (\<theta><S>))"
   using assms
 by (nominal_induct S avoiding: \<theta> Y rule: tyS.strong_induct) 
    (auto simp add: ftv_ty_subst fresh_atm)
 
 lemma ftv_Ctxt_subst:
   fixes \<Gamma>::"Ctxt"
   and   \<theta>::"Subst"
 assumes "X \<in> set (ftv \<Gamma>)"
   and   "Y \<in> set (ftv (lookup \<theta> X))"
   shows "Y \<in> set (ftv (\<theta><\<Gamma>>))"
   using assms by (induct \<Gamma>) (auto simp add: ftv_tyS_subst)
 
 lemma gen_preserved1:
   assumes "Xs \<sharp>* \<theta>"
   shows "\<theta><gen T Xs> = gen (\<theta><T>) Xs"
   using assms by (induct Xs) (auto simp add: fresh_star_def)
 
 lemma gen_preserved2:
   fixes T::"ty"
   and   \<Gamma>::"Ctxt"
   assumes "((ftv T) - (ftv \<Gamma>)) \<sharp>* \<theta>"
   shows "((ftv (\<theta><T>)) - (ftv (\<theta><\<Gamma>>))) = ((ftv T) - (ftv \<Gamma>))"
   using assms
 proof(nominal_induct T rule: ty.strong_induct)
   case (TVar tvar)
-  then show ?case
+  then show ?case 
     apply(auto simp add: fresh_star_def ftv_Ctxt_subst)
     by (metis filter.simps fresh_def fresh_psubst_Ctxt ftv_Ctxt ftv_ty.simps(1) lookup_fresh)
 next
   case (Fun ty1 ty2)
   then show ?case
     by (simp add: fresh_star_list) 
 qed
 
 lemma close_preserved:
   fixes \<Gamma>::"Ctxt"
   assumes "((ftv T) - (ftv \<Gamma>)) \<sharp>* \<theta>"
   shows "\<theta><close \<Gamma> T> = close (\<theta><\<Gamma>>) (\<theta><T>)"
   using assms by (simp add: gen_preserved1 gen_preserved2)
 
 lemma var_fresh_for_ty:
   fixes x::"var"
     and   T::"ty"
   shows "x\<sharp>T"
   by (nominal_induct T rule: ty.strong_induct) (simp_all add: fresh_atm)
 
 lemma var_fresh_for_tyS:
   fixes x::"var" and S::"tyS"
   shows "x\<sharp>S"
   by (nominal_induct S rule: tyS.strong_induct) (simp_all add: abs_fresh var_fresh_for_ty)
 
 lemma psubst_fresh_Ctxt:
   fixes x::"var" and \<Gamma>::"Ctxt" and \<theta>::"Subst"
   shows "x\<sharp>\<theta><\<Gamma>> = x\<sharp>\<Gamma>"
   by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_list_nil fresh_prod var_fresh_for_tyS)
 
 lemma psubst_valid:
   fixes \<theta>::Subst
     and   \<Gamma>::Ctxt
   assumes "valid \<Gamma>"
   shows "valid (\<theta><\<Gamma>>)"
   using assms by (induct) (auto simp add: psubst_fresh_Ctxt)
 
 lemma psubst_in:
   fixes \<Gamma>::"Ctxt"
   and   \<theta>::"Subst"
   and   pi::"tvar prm"
   and   S::"tyS"
   assumes a: "(x,S)\<in>set \<Gamma>"
   shows "(x,\<theta><S>)\<in>set (\<theta><\<Gamma>>)"
   using a by (induct \<Gamma>) (auto simp add: calc_atm)
 
 lemma typing_preserved:
   fixes \<theta>::"Subst"
     and   pi::"tvar prm"
   assumes "\<Gamma> \<turnstile> t : T"
   shows "(\<theta><\<Gamma>>) \<turnstile> t : (\<theta><T>)"
   using assms
 proof (nominal_induct \<Gamma> t T avoiding: \<theta> rule: typing.strong_induct)
   case (T_VAR \<Gamma> x S T)
   have a1: "valid \<Gamma>" by fact
   have a2: "(x, S) \<in> set \<Gamma>" by fact
   have a3: "T \<prec> S" by fact
   have  "valid (\<theta><\<Gamma>>)" using a1 by (simp add: psubst_valid)
   moreover
   have  "(x,\<theta><S>)\<in>set (\<theta><\<Gamma>>)" using a2 by (simp add: psubst_in)
   moreover
   have "\<theta><T> \<prec> \<theta><S>" using a3 by (simp add: general_preserved)
   ultimately show "(\<theta><\<Gamma>>) \<turnstile> Var x : (\<theta><T>)" by (simp add: typing.T_VAR)
 next
   case (T_APP \<Gamma> t1 T1 T2 t2)
   have "\<theta><\<Gamma>> \<turnstile> t1 : \<theta><T1 \<rightarrow> T2>" by fact
   then have "\<theta><\<Gamma>> \<turnstile> t1 : (\<theta><T1>) \<rightarrow> (\<theta><T2>)" by simp
   moreover
   have "\<theta><\<Gamma>> \<turnstile> t2 : \<theta><T1>" by fact
   ultimately show "\<theta><\<Gamma>> \<turnstile> App t1 t2 : \<theta><T2>" by (simp add: typing.T_APP)
 next
   case (T_LAM x \<Gamma> T1 t T2)
   fix pi::"tvar prm" and \<theta>::"Subst"
   have "x\<sharp>\<Gamma>" by fact
   then have "x\<sharp>\<theta><\<Gamma>>" by (simp add: psubst_fresh_Ctxt)
   moreover
   have "\<theta><((x, Ty T1)#\<Gamma>)> \<turnstile> t : \<theta><T2>" by fact
   then have "((x, Ty (\<theta><T1>))#(\<theta><\<Gamma>>)) \<turnstile> t : \<theta><T2>" by (simp add: calc_atm)
   ultimately show "\<theta><\<Gamma>> \<turnstile> Lam [x].t : \<theta><T1 \<rightarrow> T2>" by (simp add: typing.T_LAM)
 next
   case (T_LET x \<Gamma> t1 T1 t2 T2)
   have vc: "((ftv T1) - (ftv \<Gamma>)) \<sharp>* \<theta>" by fact
   have "x\<sharp>\<Gamma>" by fact
    then have a1: "x\<sharp>\<theta><\<Gamma>>" by (simp add: calc_atm psubst_fresh_Ctxt)
   have a2: "\<theta><\<Gamma>> \<turnstile> t1 : \<theta><T1>" by fact 
   have a3: "\<theta><((x, close \<Gamma> T1)#\<Gamma>)> \<turnstile> t2 : \<theta><T2>" by fact
   from a2 a3 show "\<theta><\<Gamma>> \<turnstile> Let x be t1 in t2 : \<theta><T2>"
     by (simp add: a1 better_T_LET close_preserved vc)
 qed
 
 end