diff -r bb18eed53ed6 -r a1119cf551e8 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Tue Aug 13 14:20:22 2013 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Tue Aug 13 16:25:47 2013 +0200
@@ -43,7 +43,7 @@
 
 lemma ty_cases:
   fixes T::ty
-  shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase"
+  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
@@ -53,7 +53,7 @@
 where
   "size (TBase) = 1"
 | "size (TUnit) = 1"
-| "size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2"
+| "size (T\<^sub>1\<rightarrow>T\<^sub>2) = size T\<^sub>1 + size T\<^sub>2"
 by (rule TrueI)+
 
 instance ..
@@ -97,7 +97,7 @@
   psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [100,100] 130)
 where
   "\<theta><(Var x)> = (lookup \<theta> x)"
-| "\<theta><(App t\<^isub>1 t\<^isub>2)> = App \<theta><t\<^isub>1> \<theta><t\<^isub>2>"
+| "\<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"
@@ -114,7 +114,7 @@
 
 lemma subst[simp]:
   shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
-  and   "(App t\<^isub>1 t\<^isub>2)[y::=t'] = App (t\<^isub>1[y::=t']) (t\<^isub>2[y::=t'])"
+  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"
@@ -128,10 +128,10 @@
 
 lemma subst_rename: 
   fixes c::"name"
-  assumes a: "c\<sharp>t\<^isub>1"
-  shows "t\<^isub>1[a::=t\<^isub>2] = ([(c,a)]\<bullet>t\<^isub>1)[c::=t\<^isub>2]"
+  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\<^isub>1 avoiding: a c t\<^isub>2 rule: trm.strong_induct)
+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
 
@@ -145,24 +145,24 @@
 
 lemma fresh_subst'':
   fixes z::"name"
-  assumes "z\<sharp>t\<^isub>2"
-  shows "z\<sharp>t\<^isub>1[z::=t\<^isub>2]"
+  assumes "z\<sharp>t\<^sub>2"
+  shows "z\<sharp>t\<^sub>1[z::=t\<^sub>2]"
 using assms 
-by (nominal_induct t\<^isub>1 avoiding: t\<^isub>2 z rule: trm.strong_induct)
+by (nominal_induct t\<^sub>1 avoiding: t\<^sub>2 z rule: trm.strong_induct)
    (auto simp add: abs_fresh fresh_nat fresh_atm)
 
 lemma fresh_subst':
   fixes z::"name"
-  assumes "z\<sharp>[y].t\<^isub>1" "z\<sharp>t\<^isub>2"
-  shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]"
+  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\<^isub>1 avoiding: y t\<^isub>2 z rule: trm.strong_induct)
+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)
 
 lemma fresh_subst:
   fixes z::"name"
-  assumes a: "z\<sharp>t\<^isub>1" "z\<sharp>t\<^isub>2"
-  shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]"
+  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) 
 
@@ -193,17 +193,17 @@
 
 lemma subst_fun_eq:
   fixes u::trm
-  assumes h:"[x].t\<^isub>1 = [y].t\<^isub>2"
-  shows "t\<^isub>1[x::=u] = t\<^isub>2[y::=u]"
+  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\<^isub>1=t\<^isub>2"
+    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\<^isub>1=[(x,y)] \<bullet> t\<^isub>2" and h3:"x \<sharp> t\<^isub>2"
-    then have "([(x,y)] \<bullet> t\<^isub>2)[x::=u] = t\<^isub>2[y::=u]" by (simp add: subst_rename)
+    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
@@ -275,13 +275,13 @@
 abbreviation
   "sub_context" :: "Ctxt \<Rightarrow> Ctxt \<Rightarrow> bool" (" _ \<subseteq> _ " [55,55] 55)
 where
-  "\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>a T. (a,T)\<in>set \<Gamma>\<^isub>1 \<longrightarrow> (a,T)\<in>set \<Gamma>\<^isub>2"
+  "\<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\<^isub>1)#\<Gamma> \<subseteq> (x,T\<^isub>1)#\<Gamma>'"
+ shows "(x,T\<^sub>1)#\<Gamma> \<subseteq> (x,T\<^sub>1)#\<Gamma>'"
 using a b by auto
 
 lemma fresh_context: 
@@ -295,9 +295,9 @@
 
 lemma type_unicity_in_context:
   assumes a: "valid \<Gamma>" 
-  and     b: "(x,T\<^isub>1) \<in> set \<Gamma>" 
-  and     c: "(x,T\<^isub>2) \<in> set \<Gamma>"
-  shows "T\<^isub>1=T\<^isub>2"
+  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)
@@ -306,8 +306,8 @@
   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\<^isub>1 : T\<^isub>1\<rightarrow>T\<^isub>2; \<Gamma> \<turnstile> e\<^isub>2 : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App e\<^isub>1 e\<^isub>2 : T\<^isub>2"
-| T_Lam[intro]:   "\<lbrakk>x\<sharp>\<Gamma>; (x,T\<^isub>1)#\<Gamma> \<turnstile> t : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T\<^isub>1\<rightarrow>T\<^isub>2"
+| 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"
 
@@ -344,12 +344,12 @@
   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\<^isub>1)#\<Gamma> \<turnstile> s\<^isub>2 \<equiv> t\<^isub>2 : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x]. s\<^isub>2 \<equiv>  Lam [x]. t\<^isub>2 : T\<^isub>1 \<rightarrow> T\<^isub>2"
-| Q_App[intro]:   "\<lbrakk>\<Gamma> \<turnstile> s\<^isub>1 \<equiv> t\<^isub>1 : T\<^isub>1 \<rightarrow> T\<^isub>2 ; \<Gamma> \<turnstile> s\<^isub>2 \<equiv> t\<^isub>2 : T\<^isub>1\<rbrakk> \<Longrightarrow>  \<Gamma> \<turnstile> App s\<^isub>1 s\<^isub>2 \<equiv> App t\<^isub>1 t\<^isub>2 : T\<^isub>2"
-| Q_Beta[intro]:  "\<lbrakk>x\<sharp>(\<Gamma>,s\<^isub>2,t\<^isub>2); (x,T\<^isub>1)#\<Gamma> \<turnstile> s\<^isub>1 \<equiv> t\<^isub>1 : T\<^isub>2 ; \<Gamma> \<turnstile> s\<^isub>2 \<equiv> t\<^isub>2 : T\<^isub>1\<rbrakk> 
-                   \<Longrightarrow>  \<Gamma> \<turnstile> App (Lam [x]. s\<^isub>1) s\<^isub>2 \<equiv> t\<^isub>1[x::=t\<^isub>2] : T\<^isub>2"
-| Q_Ext[intro]:   "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2\<rbrakk> 
-                   \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T\<^isub>1 \<rightarrow> T\<^isub>2"
+| 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
@@ -367,8 +367,8 @@
 inductive
   whr_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<leadsto> _" [80,80] 80) 
 where
-  QAR_Beta[intro]: "App (Lam [x]. t\<^isub>1) t\<^isub>2 \<leadsto> t\<^isub>1[x::=t\<^isub>2]"
-| QAR_App[intro]:  "t\<^isub>1 \<leadsto> t\<^isub>1' \<Longrightarrow> App t\<^isub>1 t\<^isub>2 \<leadsto> App t\<^isub>1' t\<^isub>2"
+  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]
@@ -448,11 +448,11 @@
   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\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2\<rbrakk> 
-                     \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1 \<rightarrow> T\<^isub>2"
+| 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\<^isub>1 \<rightarrow> T\<^isub>2; \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T\<^isub>2"
+| 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
@@ -466,10 +466,10 @@
 
 inductive_cases alg_equiv_inv_auto[elim]: 
   "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
-  "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
+  "\<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\<^isub>1 \<rightarrow> T\<^isub>2"
+  "\<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'"
@@ -487,12 +487,12 @@
 
 lemma Q_Arrow_strong_inversion:
   assumes fs: "x\<sharp>\<Gamma>" "x\<sharp>t" "x\<sharp>u" 
-  and h: "\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2"
-  shows "(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2"
+  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\<^isub>1)#\<Gamma> \<turnstile> App t (Var y) \<Leftrightarrow> App u (Var y) : T\<^isub>2" 
+  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\<^isub>1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) \<Leftrightarrow> [(x,y)]\<bullet> App u (Var y) : T\<^isub>2" 
+  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
@@ -518,12 +518,12 @@
   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\<^isub>1 T\<^isub>2 s t u T\<^isub>2')
-  have ih:"\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T\<^isub>1\<rightarrow>T\<^isub>2 = T" by fact
-  have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^isub>2'" by fact
-  then obtain r t T\<^isub>1' where "u = App r t"  "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
-  with ih have "T\<^isub>1\<rightarrow>T\<^isub>2 = T\<^isub>1' \<rightarrow> T\<^isub>2'" by auto
-  then show "T\<^isub>2=T\<^isub>2'" using ty.inject by auto
+  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:
@@ -552,28 +552,28 @@
   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\<^isub>1 T\<^isub>2 u)
-  have ih:"(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2 
-                                   \<Longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" by fact
+  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\<^isub>1\<rightarrow>T\<^isub>2" by fact
-  then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" using fs 
+  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\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" by simp
-  then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by (auto simp add: fresh_prod)
+  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)
 next
-  case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t u)
-  have "\<Gamma> \<turnstile> App q t \<leftrightarrow> u : T\<^isub>2" by fact
-  then obtain r T\<^isub>1' v where ha: "\<Gamma> \<turnstile> q \<leftrightarrow> r : T\<^isub>1'\<rightarrow>T\<^isub>2" and hb: "\<Gamma> \<turnstile> t \<Leftrightarrow> v : T\<^isub>1'" and eq: "u = App r v" 
+  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\<^isub>1\<rightarrow>T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
-  have ih2:"\<Gamma> \<turnstile> t \<Leftrightarrow> v : T\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> v : T\<^isub>1" by fact
-  have "\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
-  then have "\<Gamma> \<turnstile> q \<leftrightarrow> p : T\<^isub>1\<rightarrow>T\<^isub>2" by (simp add: algorithmic_symmetry)
-  with ha have "T\<^isub>1'\<rightarrow>T\<^isub>2 = T\<^isub>1\<rightarrow>T\<^isub>2" using algorithmic_path_type_unicity by simp
-  then have "T\<^isub>1' = T\<^isub>1" by (simp add: ty.inject) 
-  then have "\<Gamma> \<turnstile> s \<Leftrightarrow> v : T\<^isub>1" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T\<^isub>1\<rightarrow>T\<^isub>2" using ih1 ih2 ha hb by auto
-  then show "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T\<^isub>2" using eq 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:
@@ -587,16 +587,16 @@
   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\<^isub>1 T\<^isub>2 \<Gamma>')
+ 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\<^isub>1)#\<Gamma> \<subseteq> \<Gamma>'; valid \<Gamma>'\<rbrakk>  \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" 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\<^isub>1)#\<Gamma>')" using fs by auto
+  then have "valid ((x,T\<^sub>1)#\<Gamma>')" using fs by auto
   moreover
-  have sub: "(x,T\<^isub>1)#\<Gamma> \<subseteq> (x,T\<^isub>1)#\<Gamma>'" using h2 by auto
-  ultimately have "(x,T\<^isub>1)#\<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" using ih by simp
-  then show "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by (auto simp add: fresh_prod)
+  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)
 qed (auto)
 
 lemma path_equiv_implies_nf:
@@ -611,10 +611,10 @@
 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\<^isub>1 \<rightarrow> T\<^isub>2) =  
-    (\<forall>\<Gamma>' s' t'. \<Gamma>\<subseteq>\<Gamma>' \<longrightarrow> valid \<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^isub>1 \<longrightarrow>  (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^isub>2))"
+ | "\<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\<^isub>1 T\<^isub>2. b=T\<^isub>1 \<rightarrow> T\<^isub>2) \<or> b=TUnit \<or> b=TBase" )
+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
@@ -632,45 +632,45 @@
   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\<^isub>1 T\<^isub>2 \<Gamma>')
-  have "\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" 
+  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\<^isub>1\<rightarrow>T\<^isub>2" by simp
+  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\<^isub>1 T\<^isub>2)
+  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\<^isub>2; valid \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>2" by fact
-    have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T\<^isub>1" by fact
-    have h:"\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
+    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\<^isub>1)#\<Gamma>)" using fs by auto
-    then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T\<^isub>1" by auto
-    then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> Var x is Var x : T\<^isub>1" using ih2 by auto
-    then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) is App t (Var x) : T\<^isub>2" using h v by auto
-    then have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" using ih1 v by auto
-    then show "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by (auto simp add: fresh_prod)
+    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)
   next
     case (2 \<Gamma> p q)
-    have h: "\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
-    have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T\<^isub>2" by fact
-    have ih2:"\<And>\<Gamma> s t. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>1; valid \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" by fact
+    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\<^isub>1" and hk: "valid \<Gamma>'"
-      then have "\<Gamma>' \<turnstile> p \<leftrightarrow> q : T\<^isub>1 \<rightarrow> T\<^isub>2" using h algorithmic_monotonicity by auto
-      moreover have "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" using ih2 hl hk by auto
-      ultimately have "\<Gamma>' \<turnstile> App p s \<leftrightarrow> App q t : T\<^isub>2" by auto
-      then have "\<Gamma>' \<turnstile> App p s is App q t : T\<^isub>2" using ih1 by auto
+      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\<^isub>1\<rightarrow>T\<^isub>2"  by simp
+    then show "\<Gamma> \<turnstile> p is q : T\<^sub>1\<rightarrow>T\<^sub>2"  by simp
   }
 next
   case TBase
@@ -703,21 +703,21 @@
   case TBase
   then show "\<Gamma> \<turnstile> s is u : TBase" by (auto elim:  algorithmic_transitivity)
 next 
-  case (Arrow T\<^isub>1 T\<^isub>2 \<Gamma> s t u)
-  have h1:"\<Gamma> \<turnstile> s is t : T\<^isub>1 \<rightarrow> T\<^isub>2" by fact
-  have h2:"\<Gamma> \<turnstile> t is u : T\<^isub>1 \<rightarrow> T\<^isub>2" by fact
-  have ih1:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>1; \<Gamma> \<turnstile> t is u : T\<^isub>1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^isub>1" by fact
-  have ih2:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T\<^isub>2; \<Gamma> \<turnstile> t is u : T\<^isub>2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T\<^isub>2" by fact
+  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\<^isub>1" and hk: "valid \<Gamma>'"
-    then have "\<Gamma>' \<turnstile> u' is s' : T\<^isub>1" using logical_symmetry by blast
-    then have "\<Gamma>' \<turnstile> u' is u' : T\<^isub>1" using ih1 hl by blast
-    then have "\<Gamma>' \<turnstile> App t u' is App u u' : T\<^isub>2" using h2 hsub hk by auto
-    moreover have "\<Gamma>' \<turnstile>  App s s' is App t u' : T\<^isub>2" using h1 hsub hl hk by auto
-    ultimately have "\<Gamma>' \<turnstile>  App s s' is App u u' : T\<^isub>2" using ih2 by blast
+    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\<^isub>1 \<rightarrow> T\<^isub>2" by auto
+  then show "\<Gamma> \<turnstile> s is u : T\<^sub>1 \<rightarrow> T\<^sub>2" by auto
 qed (auto)
 
 lemma logical_weak_head_closure:
@@ -740,21 +740,21 @@
   case (TUnit \<Gamma> s t s')
   then show ?case by auto
 next 
-  case (Arrow T\<^isub>1 T\<^isub>2 \<Gamma> s t s')
+  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\<^isub>2; s' \<leadsto> s\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' is t : T\<^isub>2" by fact
-  have h2:"\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" 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\<^isub>1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^isub>2)" 
+  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\<^isub>2 t\<^isub>2
-    assume "\<Gamma> \<subseteq> \<Gamma>'" and "\<Gamma>' \<turnstile> s\<^isub>2 is t\<^isub>2 : T\<^isub>1" and "valid \<Gamma>'"
-    then have "\<Gamma>' \<turnstile> (App s s\<^isub>2) is (App t t\<^isub>2) : T\<^isub>2" using hb by auto
-    moreover have "(App s' s\<^isub>2)  \<leadsto> (App s s\<^isub>2)" using h1 by auto  
-    ultimately have "\<Gamma>' \<turnstile> App s' s\<^isub>2 is App t t\<^isub>2 : T\<^isub>2" using ih 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\<^isub>1\<rightarrow>T\<^isub>2" by auto
+  then show "\<Gamma> \<turnstile> s' is t : T\<^sub>1\<rightarrow>T\<^sub>2" by auto
 qed 
 
 abbreviation 
@@ -816,25 +816,25 @@
   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\<^isub>1 t\<^isub>2 T\<^isub>2 \<theta> \<theta>' \<Gamma>')
+  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\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><t\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
-  show "\<Gamma>' \<turnstile> \<theta><Lam [x].t\<^isub>2> is \<theta>'<Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using vc
+  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\<^isub>1" 
+    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\<^isub>1)#\<Gamma>" using equiv_subst_ext by blast
-    with ih val have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<t\<^isub>2> is ((x,t')#\<theta>')<t\<^isub>2> : T\<^isub>2" by auto
-    with vc have "\<Gamma>''\<turnstile>\<theta><t\<^isub>2>[x::=s'] is \<theta>'<t\<^isub>2>[x::=t'] : T\<^isub>2" by (simp add: psubst_subst_psubst)
+    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\<^isub>2>) s' \<leadsto> \<theta><t\<^isub>2>[x::=s']" by auto
+    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\<^isub>2>) t' \<leadsto> \<theta>'<t\<^isub>2>[x::=t']" by auto
-    ultimately show "\<Gamma>''\<turnstile> App (Lam [x].\<theta><t\<^isub>2>) s' is App (Lam [x].\<theta>'<t\<^isub>2>) t' : T\<^isub>2" 
+    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)
@@ -871,68 +871,68 @@
   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\<^isub>1 s\<^isub>2 t\<^isub>2 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
+  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\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" 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\<^isub>1" and hk: "valid \<Gamma>''"
+    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\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
-    then have "\<Gamma>'' \<turnstile> ((x,s')#\<theta>)<s\<^isub>2> is ((x,t')#\<theta>')<t\<^isub>2> : T\<^isub>2" using ih hk by blast
-    then have "\<Gamma>''\<turnstile> \<theta><s\<^isub>2>[x::=s'] is \<theta>'<t\<^isub>2>[x::=t'] : T\<^isub>2" using fs2 psubst_subst_psubst by auto
-    moreover have "App (Lam [x]. \<theta><s\<^isub>2>) s' \<leadsto>  \<theta><s\<^isub>2>[x::=s']" 
-              and "App (Lam [x].\<theta>'<t\<^isub>2>) t' \<leadsto> \<theta>'<t\<^isub>2>[x::=t']" by auto
-    ultimately have "\<Gamma>'' \<turnstile> App (Lam [x]. \<theta><s\<^isub>2>) s' is App (Lam [x].\<theta>'<t\<^isub>2>) t' : T\<^isub>2" 
+    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\<^isub>2> is Lam [x].\<theta>'<t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
-  then show "\<Gamma>' \<turnstile> \<theta><Lam [x].s\<^isub>2> is \<theta>'<Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using fs2 by auto
+  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\<^isub>1 t\<^isub>1 T\<^isub>1 T\<^isub>2 s\<^isub>2 t\<^isub>2 \<Gamma>' \<theta> \<theta>')
-  then show "\<Gamma>' \<turnstile> \<theta><App s\<^isub>1 s\<^isub>2> is \<theta>'<App t\<^isub>1 t\<^isub>2> : T\<^isub>2" by auto 
+  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\<^isub>2 t\<^isub>2 T\<^isub>1 s12 t12 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
+  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\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>1" by fact
-  have ih2: "\<And>\<Gamma>' \<theta> \<theta>'. \<lbrakk>\<Gamma>' \<turnstile> \<theta> is \<theta>' over (x,T\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><s12> is \<theta>'<t12> : T\<^isub>2" by fact
-  have "\<Gamma>' \<turnstile> \<theta><s\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>1" using ih1 h' h by auto
-  then have "\<Gamma>' \<turnstile> (x,\<theta><s\<^isub>2>)#\<theta> is (x,\<theta>'<t\<^isub>2>)#\<theta>' over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext h fs by blast
-  then have "\<Gamma>' \<turnstile> ((x,\<theta><s\<^isub>2>)#\<theta>)<s12> is ((x,\<theta>'<t\<^isub>2>)#\<theta>')<t12> : T\<^isub>2" using ih2 h' by auto
-  then have "\<Gamma>' \<turnstile> \<theta><s12>[x::=\<theta><s\<^isub>2>] is \<theta>'<t12>[x::=\<theta>'<t\<^isub>2>] : T\<^isub>2" using fs2 psubst_subst_psubst by auto
-  then have "\<Gamma>' \<turnstile> \<theta><s12>[x::=\<theta><s\<^isub>2>] is \<theta>'<t12[x::=t\<^isub>2]> : T\<^isub>2" using fs2 psubst_subst_propagate by auto
-  moreover have "App (Lam [x].\<theta><s12>) (\<theta><s\<^isub>2>) \<leadsto> \<theta><s12>[x::=\<theta><s\<^isub>2>]" by auto 
-  ultimately have "\<Gamma>' \<turnstile> App (Lam [x].\<theta><s12>) (\<theta><s\<^isub>2>) is \<theta>'<t12[x::=t\<^isub>2]> : T\<^isub>2" 
+  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\<^isub>2> is \<theta>'<t12[x::=t\<^isub>2]> : T\<^isub>2" using fs2 by simp
+  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\<^isub>1 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
+  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\<^isub>1)#\<Gamma>; valid \<Gamma>'\<rbrakk> 
-                          \<Longrightarrow> \<Gamma>' \<turnstile> \<theta><App s (Var x)> is \<theta>'<App t (Var x)> : T\<^isub>2" 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\<^isub>1" and hk: "valid \<Gamma>''"
+    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\<^isub>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\<^isub>2" using ih hk 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\<^isub>2"
+    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\<^isub>2" by auto
-    then have "\<Gamma>'' \<turnstile> App (\<theta><s>) s' is App (\<theta>'<t>) t' : T\<^isub>2" using fs fresh_psubst_simp 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\<^isub>1\<rightarrow>T\<^isub>2" by auto
+  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