
diff -r db930e490fe5 -r b61306c7987a src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Wed Mar 21 16:07:40 2007 +0100
+++ b/src/HOL/Nominal/Examples/Crary.thy	Thu Mar 22 10:35:12 2007 +0100
@@ -8,68 +8,25 @@
 (* The formalisation was done by Julien Narboux and   *)
 (* Christian Urban                                    *)
 
-(*<*)
 theory Crary
   imports "../Nominal"
 begin
 
-(* We put this def here because of some incompatibility of LatexSugar and Nominal *)
-
-syntax (Rule output)
-  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
-
-  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
-
-  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
-  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
-
-  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
-
-syntax (IfThen output)
-  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
-  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
-  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
-  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
-
-syntax (IfThenNoBox output)
-  "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
-  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
-  ("\<^raw:{\rmfamily\upshape\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\rmfamily\upshape\normalsize \,>then\<^raw:\,}>/ _.")
-  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\rmfamily\upshape\normalsize \,>and\<^raw:\,}>/ _")
-  "_asm" :: "prop \<Rightarrow> asms" ("_")
-
-
-(*>*)
-
-text {* 
-\section{Definition of the language} 
-\subsection{Definition of the terms and types} 
-
-First we define the type of atom names which will be used for binders.
-Each atom type is infinitely many atoms and equality is decidable. *}
-
 atom_decl name 
 
-text {* We define the datatype representing types. Although, It does not contain any binder we still use the \texttt{nominal\_datatype} command because the Nominal datatype package will prodive permutation functions and useful lemmas. *}
-
 nominal_datatype ty = TBase 
                     | TUnit 
                     | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100)
 
-text {* The datatype of terms contains a binder. The notation @{text "\<guillemotleft>name\<guillemotright> trm"} means that the name is bound inside trm. *}
-
 nominal_datatype trm = Unit
                      | Var "name"
                      | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100)
                      | App "trm" "trm"
                      | Const "nat"
 
-text {* As the datatype of types does not contain any binder, the application of a permutation is the identity function. In the future, this will be automatically derived by the package. *}
+types Ctxt  = "(name\<times>ty) list"
+types Subst = "(name\<times>trm) list" 
+
 
 lemma perm_ty[simp]: 
   fixes T::"ty"
@@ -88,14 +45,6 @@
   shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase"
 by (induct T rule:ty.induct_weak) (auto)
 
-text {* 
-\subsection{Size functions}
-
-We define size functions for types and terms. As Isabelle allows overloading we can use the same notation for both functions.
-
-These function are automatically generated for non nominal datatypes. In the future, we need to extend the package to generate size function for nominal datatypes as well.
- *} 
-
 instance ty :: size ..
 
 nominal_primrec
@@ -104,155 +53,263 @@
   "size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2"
 by (rule TrueI)+
 
-instance trm :: size ..
-
-nominal_primrec 
-  "size (Unit) = 1"
-  "size (Var x) = 1"
-  "size (Lam [x].t) = size t + 1"
-  "size (App t1 t2) = size t1 + size t2"
-  "size (Const n) = 1"
-apply(finite_guess)+
-apply(rule TrueI)+
-apply(simp add: fresh_nat)+
-apply(fresh_guess)+
-done
-
 lemma ty_size_greater_zero[simp]:
   fixes T::"ty"
   shows "size T > 0"
 by (nominal_induct rule:ty.induct) (simp_all)
 
-text {* 
-\subsection{Typing}
+section {* Substitutions *}
+
+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)
+
+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)
+
+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)
+
+consts
+  psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [60,100] 100)
+ 
+nominal_primrec
+  "\<theta><(Var x)> = (lookup \<theta> x)"
+  "\<theta><(App t\<^isub>1 t\<^isub>2)> = App (\<theta><t\<^isub>1>) (\<theta><t\<^isub>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
 
-\subsubsection{Typing contexts}
+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\<^isub>1 t\<^isub>2)[y::=t'] = App (t\<^isub>1[y::=t']) (t\<^isub>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.induct)
+     (perm_simp add: fresh_bij)+
 
-This section contains the definition and some properties of a typing context. As the concept of context often appears in the litterature and is general, we should in the future provide these lemmas in a library.
+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]"
+using a
+apply(nominal_induct t\<^isub>1 avoiding: a c t\<^isub>2 rule: trm.induct)
+apply(simp add: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)+
+done
+
+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.induct)
+   (auto simp add: abs_fresh lookup_fresh)
+
+lemma fresh_subst'':
+  fixes z::"name"
+  assumes "z\<sharp>t\<^isub>2"
+  shows "z\<sharp>t\<^isub>1[z::=t\<^isub>2]"
+using assms 
+by (nominal_induct t\<^isub>1 avoiding: t\<^isub>2 z rule: trm.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]"
+using assms 
+by (nominal_induct t\<^isub>1 avoiding: y t\<^isub>2 z rule: trm.induct)
+   (auto simp add: abs_fresh fresh_nat fresh_atm)
 
-\paragraph{Definition of the Validity of contexts}\strut\\
+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]"
+using a 
+by (auto simp add: 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.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)
 
-First we define what valid contexts are. Informally a context is valid is it does not contains twice the same variable.
+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.induct)
+   (auto simp add: fresh_atm abs_fresh)
+
+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]"
+proof -
+  { 
+    assume "x=y" and "t\<^isub>1=t\<^isub>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)
+    then have ?thesis using h2 by simp 
+  }
+  ultimately show ?thesis using alpha h by blast
+qed
 
-We use the following two inference rules: *}
+lemma psubst_empty[simp]:
+  shows "[]<t> = t"
+by (nominal_induct t rule: trm.induct) 
+   (auto simp add: 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.induct)
+   (auto simp add: 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)
 
-(*<*)
+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.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) 
+    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 {* Typing *}
+
 inductive2
-  valid :: "(name \<times> 'a::pt_name) list \<Rightarrow> bool"
+  valid :: "Ctxt \<Rightarrow> bool"
 where
-    v_nil[intro]:  "valid []"
-  | v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"
-(*>*)
-
-text {*
-\begin{center}
-\isastyle
-@{thm[mode=Rule] v_nil[no_vars]}{\sc{v\_nil}}
-\qquad
-@{thm[mode=Rule] v_cons[no_vars]}{\sc{v\_cons}}
-\end{center}
-*} 
-
-text{* We generate the equivariance lemma for the relation \texttt{valid}. *}
+  v_nil[intro]:  "valid []"
+| v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,T)#\<Gamma>)"
 
 nominal_inductive valid
 
-text{* We obtain a lemma called \texttt{valid\_eqvt}:
-\begin{center} 
-@{thm[mode=IfThen] valid_eqvt}
-\end{center}
-*}
-
-
-text{* We generate the inversion lemma for non empty lists. We add the \texttt{elim} attribute to tell the automated tactics to use it.
- *}
-
 inductive_cases2  
   valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)"
 
-text{*
-The generated theorem is the following:
-\begin{center}
-@{thm "valid_cons_elim_auto"[no_vars] }
-\end{center}
-*}
+abbreviation
+  "sub_context" :: "Ctxt \<Rightarrow> Ctxt \<Rightarrow> bool" (" _ \<lless> _ " [55,55] 55)
+where
+  "\<Gamma>\<^isub>1 \<lless> \<Gamma>\<^isub>2 \<equiv> \<forall>a T. (a,T)\<in>set \<Gamma>\<^isub>1 \<longrightarrow> (a,T)\<in>set \<Gamma>\<^isub>2"
 
-text{* \paragraph{Lemmas about valid contexts} 
- Now, we can prove two useful lemmas about valid contexts. 
-*}
+lemma valid_monotonicity[elim]:
+ assumes a: "\<Gamma> \<lless> \<Gamma>'" 
+ and     b: "x\<sharp>\<Gamma>'"
+ shows "(x,T\<^isub>1)#\<Gamma> \<lless> (x,T\<^isub>1)#\<Gamma>'"
+using a b by auto
 
 lemma fresh_context: 
-  fixes  \<Gamma> :: "(name\<times>ty) list"
+  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)
+using assms 
+by (induct \<Gamma>)
+   (auto simp add: fresh_prod fresh_list_cons fresh_atm)
 
 lemma type_unicity_in_context:
-  fixes  \<Gamma> :: "(name\<times>ty)list"
-  and    pi:: "name prm"
-  and    a :: "name"
-  and    \<tau> :: "ty"
-  assumes "valid \<Gamma>" and "(x,T\<^isub>1) \<in> set \<Gamma>" and "(x,T\<^isub>2) \<in> set \<Gamma>"
+  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"
-using assms by (induct \<Gamma>, auto dest!: fresh_context)
-
-text {* \paragraph{Definition of sub-contexts}
-
-The definition of sub context is standard. We do not use the subset definition to prevent the need for unfolding the definition. We include validity in the definition to shorten the statements.
- *}
-
-
-abbreviation
-  "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [55,55] 55)
-where
-  "\<Gamma>\<^isub>1 \<lless> \<Gamma>\<^isub>2 \<equiv> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>\<^isub>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>\<^isub>2) \<and> valid \<Gamma>\<^isub>2"
-
-text {* 
-\subsubsection{Definition of the typing relation}
-
-Now, we can define the typing judgements for terms. The rules are given in figure~\ref{typing}. *}
-
-(*<*)
+using a b c
+by (induct \<Gamma>)
+   (auto dest!: fresh_context)
 
 inductive2
-  typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) 
+  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_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase"
 | t_Unit[intro]:  "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit"
-(*>*)
-
-text {* 
-\begin{figure}
-\begin{center}
-\isastyle %smaller fonts
-@{thm[mode=Rule] t_Var[no_vars]}{\sc{t\_Var}}\qquad
-@{thm[mode=Rule] t_App[no_vars]}{\sc{t\_App}}\\
-@{thm[mode=Rule] t_Lam[no_vars]}{\sc{t\_Lam}}\\
-@{thm[mode=Rule] t_Const[no_vars]}{\sc{t\_Const}} \qquad
-@{thm[mode=Rule] t_Unit[no_vars]}{\sc{t\_Unit}}
-\end{center}
-\caption{Typing rules\label{typing}}
-\end{figure}
-*}
-
-lemma typing_valid:
-  assumes "\<Gamma> \<turnstile> t : T"
-  shows "valid \<Gamma>"
-  using assms by (induct)(auto)
 
 nominal_inductive typing
 
-text {* 
-\subsubsection{Inversion lemmas for the typing relation}
-
-We generate some inversion lemmas for 
-the typing judgment and add them as elimination rules for the automatic tactics.
-During the generation of these lemmas, we need the injectivity properties of the constructor of the nominal datatypes. These are not added by default in the set of simplification rules to prevent unwanted simplifications in the rest of the development. In the future, the \texttt{inductive\_cases} will be reworked to allow to use its own set of rules instead of the whole 'simpset'.
-*}
+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]
@@ -266,14 +323,9 @@
 declare trm.inject [simp del]
 declare ty.inject [simp del]
 
-text {* 
-\subsubsection{Strong induction principle}
-
-Now, we define a strong induction principle. This induction principle allow us to avoid some terms during the induction. The bound variable The avoided terms ($c$)  *}
-
 lemma typing_induct_strong
   [consumes 1, case_names t_Var t_App t_Lam t_Const t_Unit]:
-    fixes  P::"'a::fs_name \<Rightarrow> (name\<times>ty) list \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow>bool"
+    fixes  P::"'a::fs_name \<Rightarrow> Ctxt \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow>bool"
     and    x :: "'a::fs_name"
     assumes a: "\<Gamma> \<turnstile> e : T"
     and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"
@@ -328,275 +380,29 @@
   then show "P c \<Gamma> e T" by simp
 qed
 
-text {* 
-\subsection{Capture-avoiding substitutions}
-
-In this section we define parallel substitution. The usual substitution will be derived as a special case of parallel substitution. But first we define a function to lookup for the term corresponding to a type in an association list. Note that if the term does not appear in the list then we return a variable of that name.\\
-Should we return Some or None and put that in a library ?
- *}
-
-
-fun
-  lookup :: "(name\<times>trm) list \<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"
-  and   \<theta>::"(name\<times>trm) list"
-  and   X::"name"
-  shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
-by (induct \<theta>) (auto simp add: perm_bij)
-
-lemma lookup_fresh:
-  fixes z::"name"
-  assumes "z\<sharp>\<theta>" "z\<sharp>x"
-  shows "z\<sharp> lookup \<theta> x"
-using assms 
-by (induct rule: lookup.induct) (auto simp add: fresh_list_cons)
-
-lemma lookup_fresh':
-  assumes "z\<sharp>\<theta>"
-  shows "lookup \<theta> z = Var z"
-using assms 
-by (induct rule: lookup.induct)
-   (auto simp add: fresh_list_cons fresh_prod fresh_atm)
-
-text {* \subsubsection{Parallel substitution} *}
-
-consts
-  psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [60,100] 100)
- 
-nominal_primrec
-  "\<theta><(Var x)> = (lookup \<theta> x)"
-  "\<theta><(App t\<^isub>1 t\<^isub>2)> = App (\<theta><t\<^isub>1>) (\<theta><t\<^isub>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
-
-
-text {* \subsubsection{Substitution} 
-
-The substitution function is defined just as a special case of parallel substitution. 
-
-*}
-
-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\<^isub>1 t\<^isub>2)[y::=t'] = App (t\<^isub>1[y::=t']) (t\<^isub>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" 
-  and   t::"trm"
-  shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]"
-  by (nominal_induct t avoiding: x t' rule: trm.induct)
-     (perm_simp add: fresh_bij)+
-
-text {* \subsubsection{Lemmas about freshness and substitutions} *}
-
-lemma subst_rename: 
-  fixes c::"name"
-  and   t1::"trm"
-  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]"
-  using a
-  apply(nominal_induct t\<^isub>1 avoiding: a c t\<^isub>2 rule: trm.induct)
-  apply(simp add: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)+
-  done
-
-lemma fresh_psubst: 
-  fixes z::"name"
-  and   t::"trm"
-  assumes "z\<sharp>t" "z\<sharp>\<theta>"
-  shows "z\<sharp>(\<theta><t>)"
-using assms
-by (nominal_induct t avoiding: z \<theta> t rule: trm.induct)
-   (auto simp add: abs_fresh lookup_fresh)
-
-lemma fresh_subst'':
-  fixes z::"name"
-  and   t1::"trm"
-  and   t2::"trm"
-  assumes "z\<sharp>t\<^isub>2"
-  shows "z\<sharp>t\<^isub>1[z::=t\<^isub>2]"
-using assms 
-by (nominal_induct t\<^isub>1 avoiding: t\<^isub>2 z rule: trm.induct)
-   (auto simp add: abs_fresh fresh_nat fresh_atm)
+section {* Definitional Equivalence *}
 
-lemma fresh_subst':
-  fixes z::"name"
-  and   t1::"trm"
-  and   t2::"trm"
-  assumes "z\<sharp>[y].t\<^isub>1" "z\<sharp>t\<^isub>2"
-  shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]"
-using assms 
-by (nominal_induct t\<^isub>1 avoiding: y t\<^isub>2 z rule: trm.induct)
-   (auto simp add: abs_fresh fresh_nat fresh_atm)
-
-lemma fresh_subst:
-  fixes z::"name"
-  and   t1::"trm"
-  and   t2::"trm"
-  assumes "z\<sharp>t\<^isub>1" "z\<sharp>t\<^isub>2"
-  shows "z\<sharp>t\<^isub>1[y::=t\<^isub>2]"
-using assms fresh_subst'
-by (auto simp add: abs_fresh) 
-
-lemma fresh_psubst_simpl:
-  assumes "x\<sharp>t"
-  shows "(x,u)#\<theta><t> = \<theta><t>" 
-using assms
-proof (nominal_induct t avoiding: x u \<theta> rule: trm.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)
-
-lemma forget: 
-  fixes x::"name"
-  and   L::"trm"
-  assumes a: "x\<sharp>L" 
-  shows "L[x::=P] = L"
-  using a
-by (nominal_induct L avoiding: x P rule: trm.induct)
-   (auto simp add: fresh_atm abs_fresh)
-
-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]"
-proof -
-  { 
-    assume "x=y" and "t\<^isub>1=t\<^isub>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)
-    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.induct) (auto simp add: 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.induct)
-   (auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst)
-
-lemma subst_fresh_simpl:
-  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)
-
-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.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_simpl by auto
-  }
-  moreover 
-  { assume h:"x\<noteq>n"
-    then have "x\<sharp>Var n" by (auto simp add: 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)
-
-text {* 
-\section{Equivalence}
-\subsection{Definition of the equivalence relation}
- *}
-
-(*<*)
 inductive2
-  equiv_def :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<equiv> _ : _" [60,60] 60) 
+  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\<^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> s12 \<equiv> t12 : T\<^isub>2 ; \<Gamma> \<turnstile> s\<^isub>2 \<equiv> t\<^isub>2 : T\<^isub>1\<rbrakk> 
-                   \<Longrightarrow>  \<Gamma> \<turnstile> App (Lam [x]. s12) s\<^isub>2 \<equiv>  t12[x::=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"
-(*>*)
 
-text {* 
-\begin{center}
-\isastyle
-@{thm[mode=Rule] Q_Refl[no_vars]}{\sc{Q\_Refl}}\qquad
-@{thm[mode=Rule] Q_Symm[no_vars]}{\sc{Q\_Symm}}\\
-@{thm[mode=Rule] Q_Trans[no_vars]}{\sc{Q\_Trans}}\\
-@{thm[mode=Rule] Q_App[no_vars]}{\sc{Q\_App}}\\
-@{thm[mode=Rule] Q_Abs[no_vars]}{\sc{Q\_Abs}}\\
-@{thm[mode=Rule] Q_Beta[no_vars]}{\sc{Q\_Beta}}\\
-@{thm[mode=Rule] Q_Ext[no_vars]}{\sc{Q\_Ext}}\\
-\end{center}
-*}
+nominal_inductive def_equiv
 
-text {* It is now a tradition, we derive the lemma about validity, and we generate the equivariance lemma. *}
-
-lemma equiv_def_valid:
-  assumes "\<Gamma> \<turnstile> t \<equiv> s : T"
+lemma def_equiv_implies_valid:
+  assumes a: "\<Gamma> \<turnstile> t \<equiv> s : T"
   shows "valid \<Gamma>"
-using assms by (induct,auto elim:typing_valid)
+using a by (induct) (auto elim: typing_implies_valid)
 
-nominal_inductive equiv_def
-
-text{*
-\subsection{Strong induction principle for the equivalence relation}
-*}
-
-lemma equiv_def_strong_induct
+lemma def_equiv_strong_induct
   [consumes 1, case_names Q_Refl Q_Symm Q_Trans Q_Abs Q_App Q_Beta Q_Ext]:
   fixes c::"'a::fs_name"
   assumes a0: "\<Gamma> \<turnstile> s \<equiv> t : T" 
@@ -622,10 +428,10 @@
       then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>t) (pi\<bullet>T)" using a1 by (simp only: eqvt)
     next
       case (Q_Symm \<Gamma> t s T pi c)
-      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)" using a2 by (simp only: equiv_def_eqvt)
+      then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (pi\<bullet>T)" using a2 by (simp only: def_equiv_eqvt)
     next
       case (Q_Trans \<Gamma> s t T u pi c)
-      then show " P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>u) (pi\<bullet>T)" using a3 by (blast intro: equiv_def_eqvt)
+      then show " P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>u) (pi\<bullet>T)" using a3 by (blast intro: def_equiv_eqvt)
     next
       case (Q_App \<Gamma> s\<^isub>1 t\<^isub>1 T\<^isub>1 T\<^isub>2 s\<^isub>2 t\<^isub>2 pi c)
       then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App s\<^isub>1 s\<^isub>2) (pi\<bullet>App t\<^isub>1 t\<^isub>2) (pi\<bullet>T\<^isub>2)" using a5 
@@ -690,34 +496,13 @@
   then show "P c \<Gamma> s t T" by simp
 qed
 
-
-text {* \section{Type-driven equivalence algorithm} 
-
-We follow the original presentation. The algorithm is described using inference rules only.
+section {* Weak Head Reduction *}
 
-*}
-
-text {* \subsection{Weak head reduction} *}
-
-(*<*)
 inductive2
   whr_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<leadsto> _" [80,80] 80) 
 where
-  QAR_Beta[intro]: "App (Lam [x]. t12) t\<^isub>2 \<leadsto> t12[x::=t\<^isub>2]"
-| QAR_App[intro]: "t1 \<leadsto> t1' \<Longrightarrow> App t1 t\<^isub>2 \<leadsto> App t1' t\<^isub>2"
-(*>*)
-
-text {* 
-\begin{figure}
-\begin{center}
-\isastyle
-@{thm[mode=Rule] QAR_Beta[no_vars]}{\sc{QAR\_Beta}} \qquad
-@{thm[mode=Rule] QAR_App[no_vars]}{\sc{QAR\_App}}
-\end{center}
-\end{figure}
-*}
-
-text {* \subsubsection{Inversion lemma for weak head reduction} *}
+  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"
 
 declare trm.inject  [simp add]
 declare ty.inject  [simp add]
@@ -737,33 +522,24 @@
 
 nominal_inductive whr_def
 
-text {* 
-\subsection{Weak head normalization} 
-\subsubsection{Definition of the normal form}
-*}
+section {* Weak Head Normalisation *}
 
 abbreviation 
  nf :: "trm \<Rightarrow> bool" ("_ \<leadsto>|" [100] 100)
 where
   "t\<leadsto>|  \<equiv> \<not>(\<exists> u. t \<leadsto> u)" 
 
-text{* \subsubsection{Definition of weak head normal form} *}
-
-(*<*)
 inductive2
   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]
 
-text {* 
-\begin{center}
-@{thm[mode=Rule] QAN_Reduce[no_vars]}{\sc{QAN\_Reduce}}\qquad
-@{thm[mode=Rule] QAN_Normal[no_vars]}{\sc{QAN\_Normal}}
-\end{center}
-*}
+inductive_cases2 whn_inv_auto[elim]: "t \<Down> t'"
+
+declare trm.inject[simp del]
 
 lemma whn_eqvt[eqvt]:
   fixes pi::"name prm"
@@ -780,39 +556,52 @@
 apply(perm_simp)
 done
 
-text {* \subsection{Algorithmic term equivalence and algorithmic path equivalence} *}
+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_App_Lam)
+apply (clarify)
+apply (rule subst_fun_eq)
+apply (simp)
+apply (force)
+apply (erule whr_App)
+apply (blast)+
+done
 
-(*<*)
+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
+  then have "t=t'" using h red_unicity by auto
+  then show "a=b" using ih hl by auto
+qed (auto)
+
+section {* Algorithmic Term Equivalence and Algorithmic Path Equivalence *}
+
 inductive2
-  alg_equiv :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<Leftrightarrow> _ : _" [60,60] 60) 
+  alg_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<Leftrightarrow> _ : _" [60,60] 60) 
 and
-  alg_path_equiv :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60] 60) 
+  alg_path_equiv :: "Ctxt\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [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>; x\<sharp>s; x\<sharp>t; (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2\<rbrakk> 
+| 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_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_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase"
-(*>*)
-
-text {* 
-\begin{center}
-@{thm[mode=Rule] QAT_Base[no_vars]}{\sc{QAT\_Base}}\\
-@{thm[mode=Rule] QAT_Arrow[no_vars]}{\sc{QAT\_Arrow}}\\
-@{thm[mode=Rule] QAP_Var[no_vars]}{\sc{QAP\_Var}}\\
-@{thm[mode=Rule] QAP_App[no_vars]}{\sc{QAP\_App}}\\
-@{thm[mode=Rule] QAP_Const[no_vars]}{\sc{QAP\_Const}}\\
-\end{center}
-*}
-
-text {* Again we generate the equivariance lemma. *}
 
 nominal_inductive  alg_equiv
 
-text {* \subsubsection{Strong induction principle for algorithmic term and path equivalences} *}
-
 lemma alg_equiv_alg_path_equiv_strong_induct
   [case_names QAT_Base QAT_Arrow QAT_One QAP_Var QAP_App QAP_Const]:
   fixes c::"'a::fs_name"
@@ -847,8 +636,7 @@
       obtain y::"name" where fs: "y\<sharp>(pi\<bullet>s,pi\<bullet>t,pi\<bullet>\<Gamma>,c)" by (rule exists_fresh[OF fs_name1])
       let ?sw="[(pi\<bullet>x,y)]"
       let ?pi'="?sw@pi"
-      have f0: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
-      then have f1: "x\<sharp>(\<Gamma>,s,t)" by simp
+      have f1: "x\<sharp>(\<Gamma>,s,t)" by fact
       have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s,t))" using f1 by (simp add: fresh_bij)
       have f3: "y\<sharp>?pi'\<bullet>(\<Gamma>,s,t)" using f1 
 	by (simp only: pt_name2 fresh_left, auto simp add: perm_pi_simp calc_atm)
@@ -912,19 +700,11 @@
       ProjectRule.projects (ProofContext.init (the_context())) [1,2]
         (thm "alg_equiv_alg_path_equiv_strong_induct")), [])] #> snd
 *}
-(*>*)
 
-lemma alg_equiv_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)
 
-text{* \subsubsection{Inversion lemmas for algorithmic term and path equivalences} *}
-
-declare trm.inject  [simp add]
+declare trm.inject [simp add]
 declare ty.inject  [simp add]
 
-inductive_cases2 whn_inv_auto[elim]: "t \<Down> t'"
-
 inductive_cases2 alg_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<Leftrightarrow>t : TBase"
 inductive_cases2 alg_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<Leftrightarrow>t : T\<^isub>1 \<rightarrow> T\<^isub>2"
 
@@ -946,202 +726,25 @@
 declare trm.inject [simp del]
 declare ty.inject [simp del]
 
-text {* \section{Completeness of the algorithm} *}
-
-lemma algorithmic_monotonicity:
-  fixes \<Gamma>':: "(name\<times>ty) list"
-  shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T"
-  and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<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>')
-  have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
-  have h2:"\<Gamma>\<lless>\<Gamma>'" by fact
-  have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T\<^isub>1)#\<Gamma> \<lless> \<Gamma>'\<rbrakk>  \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" by fact
-  have "x\<sharp>\<Gamma>'" by fact
-  then have sub:"(x,T\<^isub>1)#\<Gamma> \<lless> (x,T\<^isub>1)#\<Gamma>'" using h2 by auto
-  then have "(x,T\<^isub>1)#\<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" using ih by auto
-  then show "\<Gamma>' \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rightarrow>T\<^isub>2" using sub fs by auto
-qed (auto)
-
-lemma valid_monotonicity[elim]:
- assumes "\<Gamma> \<lless> \<Gamma>'" and "x\<sharp>\<Gamma>'"
- shows "(x,T\<^isub>1)#\<Gamma> \<lless> (x,T\<^isub>1)#\<Gamma>'"
-using assms by auto
-
-lemma algorithmic_monotonicity_auto:
-  fixes \<Gamma>':: "(name\<times>ty) list"
-  shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T"
-  and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T"
-by (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv_strong_inducts, auto simp add: valid_monotonicity)
- 
-text {* \subsection{Definition of the logical relation} *}
-
-function log_equiv :: "((name\<times>ty) list \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool)"   
-                      ("_ \<turnstile> _ is _ : _" [60,60,60,60] 60) 
-where    
-   "\<Gamma> \<turnstile> s is t : TUnit = valid \<Gamma>"
- | "\<Gamma> \<turnstile> s is t : TBase = \<Gamma> \<turnstile> s \<Leftrightarrow> t : TBase"
- | "\<Gamma> \<turnstile> s is t : (T\<^isub>1 \<rightarrow> T\<^isub>2) =  
-           (valid \<Gamma> \<and> (\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^isub>1 \<longrightarrow>  (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^isub>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 (force)
-apply (rule ty_cases)
-done
-
-termination
-apply(relation "measure (\<lambda>(_,_,_,T). size T)")
-apply(auto)
-done
-
-lemma log_equiv_valid: 
-  assumes "\<Gamma> \<turnstile> s is t : T"
-  shows "valid \<Gamma>"
-using assms 
-by (induct rule: log_equiv.induct,auto elim: alg_equiv_valid)
-
-text {* \subsubsection{Monotonicity of the logical equivalence relation} *}
-
-lemma logical_monotonicity :
- fixes T::ty
- assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma>\<lless>\<Gamma>'" 
- shows "\<Gamma>' \<turnstile> s is t : T"
-using assms
-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\<^isub>1 T\<^isub>2 \<Gamma>')
-  then show "\<Gamma>' \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" by force 
-qed (auto)
-
-text {* If two terms are path equivalent then they are in normal form. *}
-
-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)
-
-lemma main_lemma:
-  shows "\<Gamma> \<turnstile> s is t : T \<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.induct)
-  case (Arrow T\<^isub>1 T\<^isub>2)
-  { 
-    case (1 \<Gamma> s t)
-    have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s is t : T\<^isub>2 \<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
-    obtain x::name where fs:"x\<sharp>(\<Gamma>,s,t)" by (erule exists_fresh[OF fs_name1])
-    have "valid \<Gamma>" using h log_equiv_valid by auto
-    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 by auto
-    then show "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1\<rightarrow>T\<^isub>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. \<Gamma> \<turnstile> s is t : T\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" by fact
-    {
-      fix \<Gamma>' s t
-      assume "\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s is t : T\<^isub>1"
-      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 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
-    }
-    moreover have "valid \<Gamma>" using h alg_equiv_valid by auto
-    ultimately show "\<Gamma> \<turnstile> p is q : T\<^isub>1\<rightarrow>T\<^isub>2"  by auto
-  }
-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_equiv_valid)
-
-corollary corollary_main:
-  assumes a: "\<Gamma> \<turnstile> s \<leftrightarrow> t : T"
-  shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T"
-using a main_lemma by blast
-
-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)
-
-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_App_Lam)
-apply (clarify)
-apply (rule subst_fun_eq)
-apply (simp)
-apply (force)
-apply (erule whr_App)
-apply (blast)+
-done
-
-lemma nf_unicity :
-  assumes "x \<Down> a" "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
-  then have "t=t'" using h red_unicity by auto
-  then show "a=b" using ih hl by auto
-qed (auto)
-
-nominal_inductive alg_equiv
 
 (* FIXME this lemma should not be here I am reinventing the wheel I guess *)
-(*<*)
 lemma perm_basic[simp]:
  fixes x y::"name"
 shows "[(x,y)]\<bullet>y = x"
 using assms using calc_atm by perm_simp
-(*>*)
-
-text{* \subsection{Strong inversion lemma for algorithmic equivalence} *}
 
 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"
+  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"
 proof -
-  obtain y where  fs2:"y\<sharp>\<Gamma>" "y\<sharp>u" "y\<sharp>t" 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\<^isub>1)#\<Gamma> \<turnstile> App t (Var y) \<Leftrightarrow> App u (Var y) : T\<^isub>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" 
     using  alg_equiv_eqvt[simplified] by blast
   then show ?thesis using fs fs2 by (perm_simp)
 qed
 
-text{* 
-For the \texttt{algorithmic\_transitivity} lemma we need a unicity property.
-But one has to be cautious, because this unicity property is true only for algorithmic path. 
-Indeed the following lemma is \textbf{false}:\\
-\begin{center}
-@{prop "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<Leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"}
-\end{center}
-Here is the counter example :\\
-\begin{center}
-@{prop "\<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : Tbase"} and @{prop "\<Gamma> \<turnstile> Const n \<Leftrightarrow> Const n : TUnit"}
-\end{center}
-*}
-
 (*
 lemma algorithmic_type_unicity:
   shows "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<Leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
@@ -1153,7 +756,7 @@
 *)
 
 lemma algorithmic_path_type_unicity:
-  shows "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'"
+  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')
@@ -1170,57 +773,177 @@
   then show "T\<^isub>2=T\<^isub>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)
+
 lemma algorithmic_transitivity:
-  shows "\<lbrakk> \<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; \<Gamma> \<turnstile> t \<Leftrightarrow> u : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> u : T"
-  and  "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> t \<leftrightarrow> u : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T"
+  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 h:"s \<Down> p" "t \<Down> q" by fact
-  have ih:"\<And>u. \<Gamma> \<turnstile> q \<leftrightarrow> u : TBase \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> u : TBase" by fact
   have "\<Gamma> \<turnstile> t \<Leftrightarrow> u : TBase" by fact
-  then obtain r q' where hl:"t \<Down> q'" "u \<Down> r" "\<Gamma> \<turnstile> q' \<leftrightarrow> r : TBase" by auto
-  moreover have eq:"q=q'" using nf_unicity hl h by auto
-  ultimately have "\<Gamma> \<turnstile> p \<leftrightarrow> r : TBase" using ih by auto
-  then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : TBase" using hl h by auto
+  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\<^isub>1 T\<^isub>2 u)
-  have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact
-  moreover have h:"\<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
-  moreover then obtain y where "y\<sharp>\<Gamma>" "y\<sharp>t" "y\<sharp>u" and "(y,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var y) \<Leftrightarrow> App u (Var y) : T\<^isub>2" 
-    by auto
-  moreover have fs2:"x\<sharp>u" by fact
-  ultimately have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" using Q_Arrow_strong_inversion by blast
-  moreover have ih:"\<And> v. (x,T\<^isub>1)#\<Gamma> \<turnstile> App t (Var x) \<Leftrightarrow> v : T\<^isub>2 \<Longrightarrow> (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> v : T\<^isub>2" 
-    by fact
-  ultimately have "(x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<Leftrightarrow> App u (Var x) : T\<^isub>2" by auto
-  then show "\<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" using fs fs2 by auto
+  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
+  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 
+    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)
 next
+  (* HERE *)
   case (QAP_App \<Gamma> p q T\<^isub>1 T\<^isub>2 s t u)
-  have h1:"\<Gamma> \<turnstile> p \<leftrightarrow> q : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
-  have ih1:"\<And>u. \<Gamma> \<turnstile> q \<leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2 \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> u : T\<^isub>1\<rightarrow>T\<^isub>2" by fact
-  have "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T\<^isub>1" by fact
-  have ih2:"\<And>u. \<Gamma> \<turnstile> t \<Leftrightarrow> u : T\<^isub>1 \<Longrightarrow> \<Gamma> \<turnstile> s \<Leftrightarrow> u : T\<^isub>1" by fact
   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" 
+  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" 
     by auto
-  moreover have "\<Gamma> \<turnstile> q \<leftrightarrow> p : T\<^isub>1\<rightarrow>T\<^isub>2" using h1 algorithmic_symmetry by auto
-  ultimately have "T\<^isub>1'\<rightarrow>T\<^isub>2 = T\<^isub>1\<rightarrow>T\<^isub>2" using algorithmic_path_type_unicity by auto
-  then have "T\<^isub>1' = T\<^isub>1" using ty.inject 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
 qed (auto)
 
 lemma algorithmic_weak_head_closure:
-  shows "\<lbrakk>\<Gamma> \<turnstile> s \<Leftrightarrow> t : T ; s' \<leadsto> s; t' \<leadsto> t\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' \<Leftrightarrow> t' : T"
-by (nominal_induct \<Gamma> s t T avoiding: s' t'  
+  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"])
-   (auto)
+apply(auto intro!: QAT_Arrow)
+done
+
+lemma algorithmic_monotonicity:
+  shows "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<lless> \<Gamma>' \<Longrightarrow> valid \<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<Leftrightarrow> t : T"
+  and   "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma> \<lless> \<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>')
+  have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" "x\<sharp>\<Gamma>'"by fact
+  have h2:"\<Gamma>\<lless>\<Gamma>'" by fact
+  have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T\<^isub>1)#\<Gamma> \<lless> \<Gamma>'; valid \<Gamma>'\<rbrakk>  \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) \<Leftrightarrow> App t (Var x) : T\<^isub>2" by fact
+  have "valid \<Gamma>'" by fact
+  then have "valid ((x,T\<^isub>1)#\<Gamma>')" using fs by auto
+  moreover
+  have sub: "(x,T\<^isub>1)#\<Gamma> \<lless> (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)
+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 {* Logical Equivalence *}
+
+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\<^isub>1 \<rightarrow> T\<^isub>2) =  
+    (\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<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))"
+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 (force)
+apply (rule ty_cases)
+done
+
+termination
+apply(relation "measure (\<lambda>(_,_,_,T). size T)")
+apply(auto)
+done
+
+lemma logical_monotonicity :
+ assumes a1: "\<Gamma> \<turnstile> s is t : T" 
+ and     a2: "\<Gamma>\<lless>\<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\<^isub>1 T\<^isub>2 \<Gamma>')
+  have "\<Gamma> \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>2" 
+  and  "\<Gamma> \<lless> \<Gamma>'" 
+  and  "valid \<Gamma>'" by fact
+  then show "\<Gamma>' \<turnstile> s is t : T\<^isub>1\<rightarrow>T\<^isub>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.induct)
+  case (Arrow T\<^isub>1 T\<^isub>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
+    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)
+  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
+    {
+      fix \<Gamma>' s t
+      assume "\<Gamma>\<lless>\<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
+    }
+    then show "\<Gamma> \<turnstile> p is q : T\<^isub>1\<rightarrow>T\<^isub>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.induct) (auto simp add: algorithmic_symmetry)
+by (nominal_induct arbitrary: \<Gamma> s t rule: ty.induct) 
+   (auto simp add: algorithmic_symmetry)
 
 lemma logical_transitivity:
   assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma> \<turnstile> t is u : T" 
@@ -1237,25 +960,27 @@
   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
   {
     fix \<Gamma>' s' u'
-    assume hsub:"\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s' is u' : T\<^isub>1"
+    assume hsub:"\<Gamma>\<lless>\<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 by auto
-    moreover have "\<Gamma>' \<turnstile>  App s s' is App t u' : T\<^isub>2" using h1 hsub hl by auto
+    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
   }
-  moreover have "valid \<Gamma>" using h1 alg_equiv_valid by auto
-  ultimately show "\<Gamma> \<turnstile> s is u : T\<^isub>1 \<rightarrow> T\<^isub>2" by auto
+  then show "\<Gamma> \<turnstile> s is u : T\<^isub>1 \<rightarrow> T\<^isub>2" by auto
 qed (auto)
 
 lemma logical_weak_head_closure:
-  assumes "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" "t' \<leadsto> t"
+  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 assms algorithmic_weak_head_closure 
-by (nominal_induct arbitrary: \<Gamma> s t s' t' rule:ty.induct) (auto, blast)
+using a b c algorithmic_weak_head_closure 
+by (nominal_induct arbitrary: \<Gamma> s t s' t' rule: ty.induct) 
+   (auto, blast)
 
 lemma logical_weak_head_closure':
-  assumes "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" 
+  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.induct)
@@ -1269,23 +994,23 @@
   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
-  then have hb:"\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T\<^isub>1 \<longrightarrow>  (\<Gamma>' \<turnstile> (App s s') is (App t t') : T\<^isub>2)" by auto
+  then 
+  have hb:"\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<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)" 
+    by auto
   {
     fix \<Gamma>' s\<^isub>2 t\<^isub>2
-    assume "\<Gamma>\<lless>\<Gamma>'" and "\<Gamma>' \<turnstile> s\<^isub>2 is t\<^isub>2 : T\<^isub>1"
+    assume "\<Gamma>\<lless>\<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
   }
-  moreover have "valid \<Gamma>" using h2 log_equiv_valid by auto
-  ultimately show "\<Gamma> \<turnstile> s' is t : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
+  then show "\<Gamma> \<turnstile> s' is t : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
 qed 
 
 abbreviation 
- log_equiv_subst :: "(name\<times>ty) list \<Rightarrow> (name\<times>trm) list \<Rightarrow>  (name\<times>trm) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool"  
-                     ("_ \<turnstile> _ is _ over _" [60,60] 60) 
+ log_equiv_for_psubsts :: "Ctxt \<Rightarrow> Subst \<Rightarrow> Subst \<Rightarrow> Ctxt \<Rightarrow> bool"  ("_ \<turnstile> _ is _ over _" [60,60] 60) 
 where
-  "\<Gamma>' \<turnstile> \<gamma> is \<delta> over \<Gamma> \<equiv> valid \<Gamma>' \<and> (\<forall>  x T. (x,T) \<in> set \<Gamma> \<longrightarrow> \<Gamma>' \<turnstile> \<gamma><Var x> is  \<delta><Var x> : T)"
+  "\<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>"
@@ -1297,172 +1022,180 @@
 qed
 
 lemma logical_subst_monotonicity :
-  fixes \<Gamma>::"(name\<times>ty) list"
-  and   \<Gamma>'::"(name\<times>ty) list"
-  and   \<Gamma>''::"(name\<times>ty) list"
-  assumes "\<Gamma>' \<turnstile> s is t over \<Gamma>" "\<Gamma>'\<lless>\<Gamma>''"
+  assumes a: "\<Gamma>' \<turnstile> s is t over \<Gamma>" 
+  and     b: "\<Gamma>'\<lless>\<Gamma>''"
+  and     c: "valid \<Gamma>''"
   shows "\<Gamma>'' \<turnstile> s is t over \<Gamma>"
-  using assms logical_monotonicity by blast
+using a b c logical_monotonicity by blast
 
 lemma equiv_subst_ext :
-  assumes h1:"\<Gamma>' \<turnstile> \<gamma> is \<delta> over \<Gamma>" and h2:"\<Gamma>' \<turnstile> s is t : T" and fs:"x\<sharp>\<Gamma>"
-  shows "\<Gamma>' \<turnstile> (x,s)#\<gamma> is (x,t)#\<delta> over (x,T)#\<Gamma>"
+  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)]"
-    then have "\<Gamma>' \<turnstile> (x,s)#\<gamma><Var y> is (x,t)#\<delta><Var y> : U" by auto 
+  {
+    fix y U
+    assume "(y,U) \<in> set ((x,T)#\<Gamma>)"
+    moreover
+    { 
+      assume "(y,U) \<in> set [(x,T)]"
+      then 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 "(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
   }
-  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 "(x,s)#\<gamma><Var y> = \<gamma><Var y>" "(x,t)#\<delta><Var y> = \<delta><Var y>" using fresh_psubst_simpl by blast+ 
-    moreover have  "\<Gamma>' \<turnstile> \<gamma><Var y> is \<delta><Var y> : U" using h1 hl by auto
-    ultimately have "\<Gamma>' \<turnstile> (x,s)#\<gamma><Var y> is (x,t)#\<delta><Var y> : U" by auto
-  }
-  ultimately have "\<Gamma>' \<turnstile> (x,s)#\<gamma><Var y> is (x,t)#\<delta><Var y> : U" by auto
-}
-moreover have "valid \<Gamma>'" using h2 log_equiv_valid by blast
-ultimately show "\<Gamma>' \<turnstile> (x,s)#\<gamma> is (x,t)#\<delta> over (x,T)#\<Gamma>" by auto
+  then show "\<Gamma>' \<turnstile> (x,s)#\<theta> is (x,t)#\<theta>' over (x,T)#\<Gamma>" by auto
 qed
 
-theorem fundamental_theorem:
-  assumes "\<Gamma> \<turnstile> t : T" "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>"
-  shows "\<Gamma>' \<turnstile> \<gamma><t> is \<theta><t> : T"   
-using assms
-proof (nominal_induct avoiding:\<Gamma>' \<gamma> \<theta>  rule: typing_induct_strong)
-case (t_Lam x \<Gamma> T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Gamma>' \<gamma> \<theta>)
-have fs:"x\<sharp>\<gamma>" "x\<sharp>\<theta>" "x\<sharp>\<Gamma>" by fact
-have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
-have ih:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T\<^isub>1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><t\<^isub>2> is \<theta><t\<^isub>2> : T\<^isub>2" by fact
-{
-  fix \<Gamma>'' s' t'
-  assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1"
-  then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using logical_subst_monotonicity h by blast
-  then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
-  then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><t\<^isub>2> is (x,t')#\<theta><t\<^isub>2> : T\<^isub>2" using ih by auto
-  then have "\<Gamma>''\<turnstile>\<gamma><t\<^isub>2>[x::=s'] is \<theta><t\<^isub>2>[x::=t'] : T\<^isub>2" using psubst_subst_psubst fs by simp
-  moreover have "App (Lam [x].\<gamma><t\<^isub>2>) s' \<leadsto> \<gamma><t\<^isub>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 have "\<Gamma>''\<turnstile> App (Lam [x].\<gamma><t\<^isub>2>) s' is App (Lam [x].\<theta><t\<^isub>2>) t' : T\<^isub>2" 
-    using logical_weak_head_closure by auto
-}
-moreover have "valid \<Gamma>'" using h by auto
-ultimately show "\<Gamma>' \<turnstile> \<gamma><Lam [x].t\<^isub>2> is \<theta><Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by auto 
+theorem fundamental_theorem_1:
+  assumes h1: "\<Gamma> \<turnstile> t : T" 
+  and     h2: "\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<Gamma>"
+  and     h3: "valid \<Gamma>'" 
+  shows "\<Gamma>' \<turnstile> \<theta><t> is \<theta>'<t> : T"   
+using h1 h2 h3
+proof (nominal_induct \<Gamma> t T avoiding: \<Gamma>' \<theta> \<theta>'  rule: typing_induct_strong)
+  case (t_Lam x \<Gamma> T\<^isub>1 t\<^isub>2 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
+  have fs:"x\<sharp>\<theta>" "x\<sharp>\<theta>'" "x\<sharp>\<Gamma>" by fact
+  have h:"\<Gamma>' \<turnstile> \<theta> is \<theta>' over \<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><t\<^isub>2> is \<theta>'<t\<^isub>2> : T\<^isub>2" by fact
+  {
+    fix \<Gamma>'' s' t'
+    assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1" and v: "valid \<Gamma>''"
+    then have "\<Gamma>'' \<turnstile> \<theta> is \<theta>' over \<Gamma>" using logical_subst_monotonicity h 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><t\<^isub>2> is (x,t')#\<theta>'<t\<^isub>2> : T\<^isub>2" using ih v by auto
+    then have "\<Gamma>''\<turnstile>\<theta><t\<^isub>2>[x::=s'] is \<theta>'<t\<^isub>2>[x::=t'] : T\<^isub>2" using psubst_subst_psubst fs by simp
+    moreover have "App (Lam [x].\<theta><t\<^isub>2>) s' \<leadsto> \<theta><t\<^isub>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 have "\<Gamma>''\<turnstile> App (Lam [x].\<theta><t\<^isub>2>) s' is App (Lam [x].\<theta>'<t\<^isub>2>) t' : T\<^isub>2" 
+      using logical_weak_head_closure by auto
+  }
+  then show "\<Gamma>' \<turnstile> \<theta><Lam [x].t\<^isub>2> is \<theta>'<Lam [x].t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" using fs by simp 
 qed (auto)
 
 theorem fundamental_theorem_2:
   assumes h1: "\<Gamma> \<turnstile> s \<equiv> t : T" 
-  and     h2: "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>"
-  shows "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T"
-using h1 h2
-proof (nominal_induct \<Gamma> s t T avoiding: \<Gamma>' \<gamma> \<theta> rule: equiv_def_strong_induct)
-  case (Q_Refl \<Gamma> t T \<Gamma>' \<gamma> \<theta>)
-  have "\<Gamma> \<turnstile> t : T" by fact
-  moreover have "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
-  ultimately show "\<Gamma>' \<turnstile> \<gamma><t> is \<theta><t> : T" using fundamental_theorem by blast
-next
-  case (Q_Symm \<Gamma> t s T \<Gamma>' \<gamma> \<theta>)
-  have "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
-  moreover have ih:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><t> is \<theta><s> : T" by fact
-  ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" using logical_symmetry by blast
+  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
 next
-  case (Q_Trans \<Gamma> s t T u \<Gamma>' \<gamma> \<theta>)
-  have ih1:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" by fact
-  have ih2:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><t> is \<theta><u> : T" by fact
-  have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<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 by auto
-  moreover have "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" using ih1 h by auto
-  ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><u> : T" using logical_transitivity by blast
+  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
 next
-  case (Q_Abs x \<Gamma> T\<^isub>1 s\<^isub>2 t\<^isub>2 T\<^isub>2 \<Gamma>' \<gamma> \<theta>)
+  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\<^isub>1 s\<^isub>2 t\<^isub>2 T\<^isub>2 \<Gamma>' \<theta> \<theta>')
   have fs:"x\<sharp>\<Gamma>" by fact
-  have fs2: "x\<sharp>\<gamma>" "x\<sharp>\<theta>" by fact 
-  have h2:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
-  have ih:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T\<^isub>1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s\<^isub>2> is \<theta><t\<^isub>2> : T\<^isub>2" 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
   {
     fix \<Gamma>'' s' t'
-    assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1"
-    then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using h2 logical_subst_monotonicity by blast
-    then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
-    then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><s\<^isub>2> is (x,t')#\<theta><t\<^isub>2> : T\<^isub>2" using ih by blast
-    then have "\<Gamma>''\<turnstile> \<gamma><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]. \<gamma><s\<^isub>2>) s' \<leadsto>  \<gamma><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]. \<gamma><s\<^isub>2>) s' is App (Lam [x].\<theta><t\<^isub>2>) t' : T\<^isub>2" 
+    assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>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" 
       using logical_weak_head_closure by auto
   }
   moreover have "valid \<Gamma>'" using h2 by auto
-  ultimately have "\<Gamma>' \<turnstile> Lam [x].\<gamma><s\<^isub>2> is Lam [x].\<theta><t\<^isub>2> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
-  then show "\<Gamma>' \<turnstile> \<gamma><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\<^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
 next
-  case (Q_App \<Gamma> s\<^isub>1 t\<^isub>1 T\<^isub>1 T\<^isub>2 s\<^isub>2 t\<^isub>2 \<Gamma>' \<gamma> \<theta>)
-  then show "\<Gamma>' \<turnstile> \<gamma><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\<^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 
 next
-  case (Q_Beta x \<Gamma> T\<^isub>1 s12 t12 T\<^isub>2 s\<^isub>2 t\<^isub>2 \<Gamma>' \<gamma> \<theta>)
-  have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
-  have fs:"x\<sharp>\<Gamma>" by fact
-  have fs2:"x\<sharp>\<gamma>" "x\<sharp>\<theta>" by fact 
-  have ih1:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s\<^isub>2> is \<theta><t\<^isub>2> : T\<^isub>1" by fact
-  have ih2:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T\<^isub>1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s12> is \<theta><t12> : T\<^isub>2" by fact
-  have "\<Gamma>' \<turnstile> \<gamma><s\<^isub>2> is \<theta><t\<^isub>2> : T\<^isub>1" using ih1 h by auto
-  then have "\<Gamma>' \<turnstile> (x,\<gamma><s\<^isub>2>)#\<gamma> 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,\<gamma><s\<^isub>2>)#\<gamma><s12> is (x,\<theta><t\<^isub>2>)#\<theta><t12> : T\<^isub>2" using ih2 by auto
-  then have "\<Gamma>' \<turnstile> \<gamma><s12>[x::=\<gamma><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> \<gamma><s12>[x::=\<gamma><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].\<gamma><s12>) (\<gamma><s\<^isub>2>) \<leadsto> \<gamma><s12>[x::=\<gamma><s\<^isub>2>]" by auto 
-  ultimately have "\<Gamma>' \<turnstile> App (Lam [x].\<gamma><s12>) (\<gamma><s\<^isub>2>) is \<theta><t12[x::=t\<^isub>2]> : T\<^isub>2" 
+  case (Q_Beta x \<Gamma> T\<^isub>1 s12 t12 T\<^isub>2 s\<^isub>2 t\<^isub>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" 
     using logical_weak_head_closure' by auto
-  then show "\<Gamma>' \<turnstile> \<gamma><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\<^isub>2> is \<theta>'<t12[x::=t\<^isub>2]> : T\<^isub>2" using fs2 by simp
 next
-  case (Q_Ext x \<Gamma> s t T\<^isub>1 T\<^isub>2 \<Gamma>' \<gamma> \<theta>)
-  have h2:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact
+  case (Q_Ext x \<Gamma> s t T\<^isub>1 T\<^isub>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>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T\<^isub>1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><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\<^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
    {
     fix \<Gamma>'' s' t'
-    assume hsub:"\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T\<^isub>1"
-    then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using h2 logical_subst_monotonicity by blast
-    then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T\<^isub>1)#\<Gamma>" using equiv_subst_ext hl fs by blast
-    then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><App s (Var x)>  is (x,t')#\<theta><App t (Var x)> : T\<^isub>2" using ih by blast
-    then have "\<Gamma>'' \<turnstile> App (((x,s')#\<gamma>)<s>) (((x,s')#\<gamma>)<(Var x)>) is App ((x,t')#\<theta><t>) ((x,t')#\<theta><(Var x)>) : T\<^isub>2"
+    assume hsub: "\<Gamma>'\<lless>\<Gamma>''" and hl: "\<Gamma>''\<turnstile> s' is t' : T\<^isub>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> App (((x,s')#\<theta>)<s>) (((x,s')#\<theta>)<(Var x)>) is App ((x,t')#\<theta>'<t>) ((x,t')#\<theta>'<(Var x)>) : T\<^isub>2"
       by auto
-    then have "\<Gamma>'' \<turnstile> App ((x,s')#\<gamma><s>) s'  is App ((x,t')#\<theta><t>) t' : T\<^isub>2" by auto
-    then have "\<Gamma>'' \<turnstile> App (\<gamma><s>) s' is App (\<theta><t>) t' : T\<^isub>2" using fs fresh_psubst_simpl 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
   }
   moreover have "valid \<Gamma>'" using h2 by auto
-  ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
+  ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
 qed
 
 
 theorem completeness:
-  assumes "\<Gamma> \<turnstile> s \<equiv> t : T"
+  assumes asm: "\<Gamma> \<turnstile> s \<equiv> t : T"
   shows   "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T"
-using assms
 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 by blast
+    then have "\<Gamma> \<turnstile> Var x is Var x : T" using main_lemma(2) by blast
   }
-  moreover have "valid \<Gamma>" using equiv_def_valid assms by auto
   ultimately have "\<Gamma> \<turnstile> [] is [] over \<Gamma>" by auto 
-  then have "\<Gamma> \<turnstile> []<s> is []<t> : T" using fundamental_theorem_2 assms by blast
+  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 by simp
+  then show  "\<Gamma> \<turnstile> s \<Leftrightarrow> t : T" using main_lemma(1) val by simp
 qed
 
-text{*
-\section{About soundness}
-*}
 
 text {* We leave soundness as an exercise - like in the 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"} \\




