src/HOL/Nominal/Examples/Class1.thy

 theory Class1
-imports "HOL-Nominal.Nominal" 
+imports "HOL-Nominal.Nominal"
 begin
 
 section \<open>Term-Calculus from Urban's PhD\<close>
 
 atom_decl name coname

   fixes a::"coname"
   and   x::"name"
   and   T::"ty"
   shows "a\<sharp>T" and "x\<sharp>T"
 by (nominal_induct T rule: ty.strong_induct)
-   (auto simp add: fresh_string)
-
-text \<open>terms\<close>
+   (auto simp: fresh_string)
+
+text \<open>terms\<close>                               
 
 nominal_datatype trm = 
     Ax   "name" "coname"
   | Cut  "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm"            ("Cut <_>._ (_)._" [100,100,100,100] 100)
   | NotR "\<guillemotleft>name\<guillemotright>trm" "coname"                 ("NotR (_)._ _" [100,100,100] 100)

 | "a\<sharp>(d,e,b) \<Longrightarrow> (OrR2 <a>.M b)[d\<turnstile>c>e] = (if b=d then OrR2 <a>.(M[d\<turnstile>c>e]) e else OrR2 <a>.(M[d\<turnstile>c>e]) b)"
 | "\<lbrakk>x\<sharp>(N,z);y\<sharp>(M,z);y\<noteq>x\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N z)[d\<turnstile>c>e] = OrL (x).(M[d\<turnstile>c>e]) (y).(N[d\<turnstile>c>e]) z"
 | "a\<sharp>(d,e,b) \<Longrightarrow> (ImpR (x).<a>.M b)[d\<turnstile>c>e] = 
        (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)"
 | "\<lbrakk>a\<sharp>(d,e,N);x\<sharp>(M,y)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y)[d\<turnstile>c>e] = ImpL <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e]) y"
-apply(finite_guess)+
-apply(rule TrueI)+
-apply(simp add: abs_fresh abs_supp fin_supp)+
-apply(fresh_guess)+
-done
+  by(finite_guess | simp add: abs_fresh abs_supp fin_supp | fresh_guess)+
 
 nominal_primrec (freshness_context: "(u::name,v::name)") 
   nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"      ("_[_\<turnstile>n>_]" [100,100,100] 100) 
 where
   "(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)" 

 | "\<lbrakk>x\<sharp>(u,v,N,z);y\<sharp>(u,v,M,z);y\<noteq>x\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N z)[u\<turnstile>n>v] = 
         (if z=u then OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) v else OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) z)"
 | "\<lbrakk>a\<sharp>b; x\<sharp>(u,v)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b)[u\<turnstile>n>v] = ImpR (x).<a>.(M[u\<turnstile>n>v]) b"
 | "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M,y)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] = 
         (if y=u then ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) v else ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) y)"
-apply(finite_guess)+
-apply(rule TrueI)+
-apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1)+
-apply(fresh_guess)+
-done
+  by(finite_guess | simp add: abs_fresh abs_supp fin_supp | fresh_guess)+
 
 lemmas eq_bij = pt_bij[OF pt_name_inst, OF at_name_inst] pt_bij[OF pt_coname_inst, OF at_coname_inst]
 
 lemma crename_name_eqvt[eqvt]:
   fixes pi::"name prm"
   shows "pi\<bullet>(M[d\<turnstile>c>e]) = (pi\<bullet>M)[(pi\<bullet>d)\<turnstile>c>(pi\<bullet>e)]"
-apply(nominal_induct M avoiding: d e rule: trm.strong_induct)
-apply(auto simp add: fresh_bij eq_bij)
-done
+  by (nominal_induct M avoiding: d e rule: trm.strong_induct) (auto simp: fresh_bij eq_bij)
 
 lemma crename_coname_eqvt[eqvt]:
   fixes pi::"coname prm"
   shows "pi\<bullet>(M[d\<turnstile>c>e]) = (pi\<bullet>M)[(pi\<bullet>d)\<turnstile>c>(pi\<bullet>e)]"
-apply(nominal_induct M avoiding: d e rule: trm.strong_induct)
-apply(auto simp add: fresh_bij eq_bij)
-done
+  by (nominal_induct M avoiding: d e rule: trm.strong_induct)(auto simp: fresh_bij eq_bij)
 
 lemma nrename_name_eqvt[eqvt]:
   fixes pi::"name prm"
   shows "pi\<bullet>(M[x\<turnstile>n>y]) = (pi\<bullet>M)[(pi\<bullet>x)\<turnstile>n>(pi\<bullet>y)]"
-apply(nominal_induct M avoiding: x y rule: trm.strong_induct)
-apply(auto simp add: fresh_bij eq_bij)
-done
+  by(nominal_induct M avoiding: x y rule: trm.strong_induct) (auto simp: fresh_bij eq_bij)
 
 lemma nrename_coname_eqvt[eqvt]:
   fixes pi::"coname prm"
   shows "pi\<bullet>(M[x\<turnstile>n>y]) = (pi\<bullet>M)[(pi\<bullet>x)\<turnstile>n>(pi\<bullet>y)]"
-apply(nominal_induct M avoiding: x y rule: trm.strong_induct)
-apply(auto simp add: fresh_bij eq_bij)
-done
+  by(nominal_induct M avoiding: x y rule: trm.strong_induct)(auto simp: fresh_bij eq_bij)
 
 lemmas rename_eqvts = crename_name_eqvt crename_coname_eqvt
                       nrename_name_eqvt nrename_coname_eqvt
 lemma nrename_fresh:
   assumes a: "x\<sharp>M"
   shows "M[x\<turnstile>n>y] = M"
 using a
 by (nominal_induct M avoiding: x y rule: trm.strong_induct)
-   (auto simp add: trm.inject fresh_atm abs_fresh fin_supp abs_supp)
+   (auto simp: trm.inject fresh_atm abs_fresh fin_supp abs_supp)
 
 lemma crename_fresh:
   assumes a: "a\<sharp>M"
   shows "M[a\<turnstile>c>b] = M"
 using a
 by (nominal_induct M avoiding: a b rule: trm.strong_induct)
-   (auto simp add: trm.inject fresh_atm abs_fresh)
+   (auto simp: trm.inject fresh_atm abs_fresh)
 
 lemma nrename_nfresh:
   fixes x::"name"
   shows "x\<sharp>y\<Longrightarrow>x\<sharp>M[x\<turnstile>n>y]"
 by (nominal_induct M avoiding: x y rule: trm.strong_induct)
-   (auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
+   (auto simp: fresh_atm abs_fresh abs_supp fin_supp)
 
  lemma crename_nfresh:
   fixes x::"name"
   shows "x\<sharp>M\<Longrightarrow>x\<sharp>M[a\<turnstile>c>b]"
 by (nominal_induct M avoiding: a b rule: trm.strong_induct)
-   (auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
+   (auto simp: fresh_atm abs_fresh abs_supp fin_supp)
 
 lemma crename_cfresh:
   fixes a::"coname"
   shows "a\<sharp>b\<Longrightarrow>a\<sharp>M[a\<turnstile>c>b]"
 by (nominal_induct M avoiding: a b rule: trm.strong_induct)
-   (auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
+   (auto simp: fresh_atm abs_fresh abs_supp fin_supp)
 
 lemma nrename_cfresh:
   fixes c::"coname"
   shows "c\<sharp>M\<Longrightarrow>c\<sharp>M[x\<turnstile>n>y]"
 by (nominal_induct M avoiding: x y rule: trm.strong_induct)
-   (auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
+   (auto simp: fresh_atm abs_fresh abs_supp fin_supp)
 
 lemma nrename_nfresh':
   fixes x::"name"
   shows "x\<sharp>(M,z,y)\<Longrightarrow>x\<sharp>M[z\<turnstile>n>y]"
 by (nominal_induct M avoiding: x z y rule: trm.strong_induct)
-   (auto simp add: fresh_prod fresh_atm abs_fresh abs_supp fin_supp)
+   (auto simp: fresh_prod fresh_atm abs_fresh abs_supp fin_supp)
 
 lemma crename_cfresh':
   fixes a::"coname"
   shows "a\<sharp>(M,b,c)\<Longrightarrow>a\<sharp>M[b\<turnstile>c>c]"
 by (nominal_induct M avoiding: a b c rule: trm.strong_induct)
-   (auto simp add: fresh_prod fresh_atm abs_fresh abs_supp fin_supp)
+   (auto simp: fresh_prod fresh_atm abs_fresh abs_supp fin_supp)
 
 lemma nrename_rename:
   assumes a: "x'\<sharp>M"
   shows "([(x',x)]\<bullet>M)[x'\<turnstile>n>y]= M[x\<turnstile>n>y]"
 using a
 apply(nominal_induct M avoiding: x x' y rule: trm.strong_induct)
-apply(auto simp add: abs_fresh fresh_bij fresh_atm fresh_prod fresh_right calc_atm abs_supp fin_supp)
-apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)
+apply(auto simp: abs_fresh fresh_bij fresh_atm fresh_prod fresh_right calc_atm abs_supp fin_supp)
+apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)
 done
 
 lemma crename_rename:
   assumes a: "a'\<sharp>M"
   shows "([(a',a)]\<bullet>M)[a'\<turnstile>c>b]= M[a\<turnstile>c>b]"
 using a
 apply(nominal_induct M avoiding: a a' b rule: trm.strong_induct)
-apply(auto simp add: abs_fresh fresh_bij fresh_atm fresh_prod fresh_right calc_atm abs_supp fin_supp)
-apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)
+apply(auto simp: abs_fresh fresh_bij fresh_atm fresh_prod fresh_right calc_atm abs_supp fin_supp)
+apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)
 done
 
 lemmas rename_fresh = nrename_fresh crename_fresh 
                       nrename_nfresh crename_nfresh crename_cfresh nrename_cfresh
                       nrename_nfresh' crename_cfresh'

   shows "(Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])"
 proof -
   obtain x'::"name"   where fs1: "x'\<sharp>(M,N,a,x,u,v)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a,x,u,v)" by (rule exists_fresh(2), rule fin_supp, blast)
   have eq1: "(Cut <a>.M (x).N) = (Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N))"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   have "(Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N))[u\<turnstile>n>v] = 
                         Cut <a'>.(([(a',a)]\<bullet>M)[u\<turnstile>n>v]) (x').(([(x',x)]\<bullet>N)[u\<turnstile>n>v])"
     using fs1 fs2
-    apply -
-    apply(rule nrename.simps)
-    apply(simp add: fresh_left calc_atm)
-    apply(simp add: fresh_left calc_atm)
-    done
+    by (intro nrename.simps; simp add: fresh_left calc_atm)
   also have "\<dots> = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])" using fs1 fs2 a
-    apply -
-    apply(simp add: trm.inject alpha fresh_atm fresh_prod rename_eqvts)
-    apply(simp add: calc_atm)
-    apply(simp add: rename_fresh fresh_atm)
-    done
+    by(simp add: trm.inject alpha fresh_prod rename_eqvts calc_atm rename_fresh fresh_atm)
   finally show "(Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])" using eq1
     by simp
 qed
 
 lemma better_crename_Cut:

   shows "(Cut <a>.M (x).N)[b\<turnstile>c>c] = Cut <a>.(M[b\<turnstile>c>c]) (x).(N[b\<turnstile>c>c])"
 proof -
   obtain x'::"name"   where fs1: "x'\<sharp>(M,N,a,x,b,c)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a,x,b,c)" by (rule exists_fresh(2), rule fin_supp, blast)
   have eq1: "(Cut <a>.M (x).N) = (Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N))"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   have "(Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N))[b\<turnstile>c>c] = 
                         Cut <a'>.(([(a',a)]\<bullet>M)[b\<turnstile>c>c]) (x').(([(x',x)]\<bullet>N)[b\<turnstile>c>c])"
     using fs1 fs2
-    apply -
-    apply(rule crename.simps)
-    apply(simp add: fresh_left calc_atm)
-    apply(simp add: fresh_left calc_atm)
-    done
+    by (intro crename.simps; simp add: fresh_left calc_atm)
   also have "\<dots> = Cut <a>.(M[b\<turnstile>c>c]) (x).(N[b\<turnstile>c>c])" using fs1 fs2 a
-    apply -
-    apply(simp add: trm.inject alpha fresh_atm fresh_prod rename_eqvts)
-    apply(simp add: calc_atm)
-    apply(simp add: rename_fresh fresh_atm)
-    done
+    by(simp add: trm.inject alpha calc_atm rename_fresh fresh_atm fresh_prod rename_eqvts)
   finally show "(Cut <a>.M (x).N)[b\<turnstile>c>c] = Cut <a>.(M[b\<turnstile>c>c]) (x).(N[b\<turnstile>c>c])" using eq1
     by simp
 qed
 
 lemma crename_id:

   fixes c::"coname"
   and   pi::"coname prm"
   and   M::"trm"
   assumes a: "c\<sharp>pi" "c\<sharp>M"
   shows "c\<sharp>(pi\<bullet>M)"
-using a
-apply -
-apply(simp add: fresh_left)
-apply(simp add: at_prm_fresh[OF at_coname_inst] fresh_list_rev)
-done
+  by (simp add: assms fresh_perm_app)
 
 lemma fresh_perm_name:
   fixes x::"name"
   and   pi::"name prm"
   and   M::"trm"
   assumes a: "x\<sharp>pi" "x\<sharp>M"
   shows "x\<sharp>(pi\<bullet>M)"
-using a
-apply -
-apply(simp add: fresh_left)
-apply(simp add: at_prm_fresh[OF at_name_inst] fresh_list_rev)
-done
+  by (simp add: assms fresh_perm_app)
 
 lemma fresh_fun_simp_NotL:
   assumes a: "x'\<sharp>P" "x'\<sharp>M"
   shows "fresh_fun (\<lambda>x'. Cut <c>.P (x').NotL <a>.M x') = Cut <c>.P (x').NotL <a>.M x'"
-using a
-apply -
-apply(rule fresh_fun_app)
-apply(rule pt_name_inst)
-apply(rule at_name_inst)
-apply(finite_guess)
-apply(subgoal_tac "\<exists>n::name. n\<sharp>(c,P,a,M)")
-apply(erule exE)
-apply(rule_tac x="n" in exI)
-apply(simp add: fresh_prod abs_fresh)
-apply(fresh_guess)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(fresh_guess)
-done
+proof (rule fresh_fun_app)
+  show "pt (TYPE(trm)::trm itself) (TYPE(name)::name itself)"
+    by(rule pt_name_inst)
+  show "at (TYPE(name)::name itself)"
+    by(rule at_name_inst)
+  show "finite (supp (\<lambda>x'. Cut <c>.P (x').NotL <a>.M x')::name set)"
+    using a by(finite_guess)
+  obtain n::name where n: "n\<sharp>(c,P,a,M)"
+    by (metis assms fresh_atm(3) fresh_prod)
+  with assms
+  show "\<exists>b. b \<sharp> (\<lambda>x'. Cut <c>.P (x').NotL <a>.M x', Cut <c>.P (b).NotL <a>.M b)"
+    apply(intro exI [where x="n"])
+    apply(simp add: fresh_prod abs_fresh)
+    apply(fresh_guess)
+    done
+  show "x' \<sharp> (\<lambda>x'. Cut <c>.P (x').NotL <a>.M x')"
+    using assms by(fresh_guess)
+qed
 
 lemma fresh_fun_NotL[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
   shows "pi1\<bullet>fresh_fun (\<lambda>x'. Cut <c>.P (x').NotL <a>.M x')=
              fresh_fun (pi1\<bullet>(\<lambda>x'. Cut <c>.P (x').NotL <a>.M x'))"
   and   "pi2\<bullet>fresh_fun (\<lambda>x'. Cut <c>.P (x').NotL <a>.M x')=
              fresh_fun (pi2\<bullet>(\<lambda>x'. Cut <c>.P (x').NotL <a>.M x'))"
-apply -
-apply(perm_simp)
-apply(generate_fresh "name")
-apply(auto simp add: fresh_prod)
-apply(simp add: fresh_fun_simp_NotL)
-apply(rule sym)
-apply(rule trans)
-apply(rule fresh_fun_simp_NotL)
-apply(rule fresh_perm_name)
-apply(assumption)
-apply(assumption)
-apply(rule fresh_perm_name)
-apply(assumption)
-apply(assumption)
-apply(simp add: at_prm_fresh[OF at_name_inst] swap_simps)
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,pi2\<bullet>P,pi2\<bullet>M,pi2)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_NotL calc_atm)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-done
+   apply(perm_simp)
+   apply(generate_fresh "name")
+   apply(auto simp: fresh_prod fresh_fun_simp_NotL)
+   apply(rule sym)
+   apply(rule trans)
+    apply(rule fresh_fun_simp_NotL)
+     apply(blast intro: fresh_perm_name)
+    apply(metis fresh_perm_name)
+   apply(simp add: at_prm_fresh[OF at_name_inst] swap_simps)
+
+  apply(perm_simp)
+  apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,pi2\<bullet>P,pi2\<bullet>M,pi2)")
+   apply (metis fresh_fun_simp_NotL fresh_prodD swap_simps(8) trm.perm(14) trm.perm(16))
+  by (meson exists_fresh(1) fs_name1)
 
 lemma fresh_fun_simp_AndL1:
   assumes a: "z'\<sharp>P" "z'\<sharp>M" "z'\<sharp>x"
-  shows "fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).M z') = Cut <c>.P (z').AndL1 (x).M z'"
-using a
-apply -
-apply(rule fresh_fun_app)
-apply(rule pt_name_inst)
-apply(rule at_name_inst)
-apply(finite_guess)
-apply(subgoal_tac "\<exists>n::name. n\<sharp>(c,P,x,M)")
-apply(erule exE)
-apply(rule_tac x="n" in exI)
-apply(simp add: fresh_prod abs_fresh)
-apply(fresh_guess)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(fresh_guess)
-done
+  shows "fresh_fun (\<lambda>z'. Cut <c>.P(z').AndL1 (x).M z') = Cut <c>.P (z').AndL1 (x).M z'"
+proof (rule fresh_fun_app [OF pt_name_inst at_name_inst])
+  obtain n::name where "n\<sharp>(c,P,x,M)"
+    by (meson exists_fresh(1) fs_name1)
+  then show "\<exists>a. a \<sharp> (\<lambda>z'. Cut <c>.P(z').AndL1 x. M z', Cut <c>.P(a).AndL1 x. M a)"
+    apply(intro exI [where x="n"])
+    apply(simp add: fresh_prod abs_fresh)
+    apply(fresh_guess)
+    done
+next
+  show "z' \<sharp> (\<lambda>z'. Cut <c>.P(z').AndL1 x. M z')"
+    using a by(fresh_guess)
+qed finite_guess
 
 lemma fresh_fun_AndL1[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
   shows "pi1\<bullet>fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).M z')=
              fresh_fun (pi1\<bullet>(\<lambda>z'. Cut <c>.P (z').AndL1 (x).M z'))"
   and   "pi2\<bullet>fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).M z')=
              fresh_fun (pi2\<bullet>(\<lambda>z'. Cut <c>.P (z').AndL1 (x).M z'))"
-apply -
 apply(perm_simp)
 apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,x,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>x,pi1)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_AndL1 at_prm_fresh[OF at_name_inst] swap_simps)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
+apply(force simp add: fresh_prod fresh_fun_simp_AndL1 at_prm_fresh[OF at_name_inst] swap_simps)
+  apply (meson exists_fresh(1) fs_name1)
 apply(perm_simp)
 apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,x,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>x,pi2)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_AndL1 calc_atm)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-done
+apply(force simp add: fresh_prod fresh_fun_simp_AndL1 calc_atm)
+  by (meson exists_fresh'(1) fs_name1)
 
 lemma fresh_fun_simp_AndL2:
   assumes a: "z'\<sharp>P" "z'\<sharp>M" "z'\<sharp>x"
   shows "fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).M z') = Cut <c>.P (z').AndL2 (x).M z'"
-using a
-apply -
-apply(rule fresh_fun_app)
-apply(rule pt_name_inst)
-apply(rule at_name_inst)
-apply(finite_guess)
-apply(subgoal_tac "\<exists>n::name. n\<sharp>(c,P,x,M)")
-apply(erule exE)
-apply(rule_tac x="n" in exI)
-apply(simp add: fresh_prod abs_fresh)
-apply(fresh_guess)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(fresh_guess)
-done
+proof (rule fresh_fun_app [OF pt_name_inst at_name_inst])
+  obtain n::name where "n\<sharp>(c,P,x,M)"
+    by (meson exists_fresh(1) fs_name1)
+  then show "\<exists>a. a \<sharp> (\<lambda>z'. Cut <c>.P(z').AndL2 x. M z', Cut <c>.P(a).AndL2 x. M a)"
+    apply(intro exI [where x="n"])
+    apply(simp add: fresh_prod abs_fresh)
+    apply(fresh_guess)
+    done
+next
+  show "z' \<sharp> (\<lambda>z'. Cut <c>.P(z').AndL2 x. M z')"
+    using a by(fresh_guess)           
+qed finite_guess
 
 lemma fresh_fun_AndL2[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
   shows "pi1\<bullet>fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).M z')=
              fresh_fun (pi1\<bullet>(\<lambda>z'. Cut <c>.P (z').AndL2 (x).M z'))"
   and   "pi2\<bullet>fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).M z')=
              fresh_fun (pi2\<bullet>(\<lambda>z'. Cut <c>.P (z').AndL2 (x).M z'))"
-apply -
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,x,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>x,pi1)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_AndL2 at_prm_fresh[OF at_name_inst] swap_simps)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,x,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>x,pi2)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_AndL2 calc_atm)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-done
+   apply(perm_simp)
+   apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,x,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>x,pi1)")
+    apply(force simp add: fresh_prod fresh_fun_simp_AndL2 at_prm_fresh[OF at_name_inst] swap_simps)
+   apply (meson exists_fresh(1) fs_name1)
+  apply(perm_simp)
+  apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,x,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>x,pi2)")
+   apply(force simp add: fresh_prod fresh_fun_simp_AndL2 calc_atm)
+  by (meson exists_fresh(1) fs_name1)
 
 lemma fresh_fun_simp_OrL:
   assumes a: "z'\<sharp>P" "z'\<sharp>M" "z'\<sharp>N" "z'\<sharp>u" "z'\<sharp>x"
-  shows "fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (x).M (u).N z') = Cut <c>.P (z').OrL (x).M (u).N z'"
-using a
-apply -
-apply(rule fresh_fun_app)
-apply(rule pt_name_inst)
-apply(rule at_name_inst)
-apply(finite_guess)
-apply(subgoal_tac "\<exists>n::name. n\<sharp>(c,P,x,M,u,N)")
-apply(erule exE)
-apply(rule_tac x="n" in exI)
-apply(simp add: fresh_prod abs_fresh)
-apply(fresh_guess)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(fresh_guess)
-done
+  shows "fresh_fun (\<lambda>z'. Cut <c>.P(z').OrL(x).M(u).N z') = Cut <c>.P (z').OrL (x).M (u).N z'"
+proof (rule fresh_fun_app [OF pt_name_inst at_name_inst])
+  obtain n::name where "n\<sharp>(c,P,x,M,u,N)"
+    by (meson exists_fresh(1) fs_name1)
+  then show "\<exists>a. a \<sharp> (\<lambda>z'. Cut <c>.P(z').OrL(x).M(u).N(z'), Cut <c>.P(a).OrL(x).M(u).N(a))"
+    apply(intro exI [where x="n"])
+    apply(simp add: fresh_prod abs_fresh)
+    apply(fresh_guess)
+    done
+next
+  show "z' \<sharp> (\<lambda>z'. Cut <c>.P(z').OrL(x).M(u).N(z'))"
+    using a by(fresh_guess) 
+qed finite_guess
 
 lemma fresh_fun_OrL[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
-  shows "pi1\<bullet>fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (x).M (u).N z')=
-             fresh_fun (pi1\<bullet>(\<lambda>z'. Cut <c>.P (z').OrL (x).M (u).N z'))"
-  and   "pi2\<bullet>fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (x).M (u).N z')=
-             fresh_fun (pi2\<bullet>(\<lambda>z'. Cut <c>.P (z').OrL (x).M (u).N z'))"
-apply -
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,N,x,u,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>N,pi1\<bullet>x,pi1\<bullet>u,pi1)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_OrL at_prm_fresh[OF at_name_inst] swap_simps)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,N,x,u,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>N,pi2\<bullet>x,pi2\<bullet>u,pi2)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_OrL calc_atm)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-done
+  shows "pi1\<bullet>fresh_fun (\<lambda>z'. Cut <c>.P(z').OrL (x).M(u).N z')=
+             fresh_fun (pi1\<bullet>(\<lambda>z'. Cut <c>.P (z').OrL(x).M (u).N z'))"
+  and   "pi2\<bullet>fresh_fun (\<lambda>z'. Cut <c>.P(z').OrL (x).M(u).N z')=
+             fresh_fun (pi2\<bullet>(\<lambda>z'. Cut <c>.P(z').OrL(x).M(u).N z'))"
+   apply(perm_simp)
+   apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,N,x,u,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>N,pi1\<bullet>x,pi1\<bullet>u,pi1)")
+    apply(force simp add: fresh_prod fresh_fun_simp_OrL at_prm_fresh[OF at_name_inst] swap_simps)
+   apply (meson exists_fresh(1) fs_name1)
+  apply(perm_simp)
+  apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,N,x,u,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>N,pi2\<bullet>x,pi2\<bullet>u,pi2)")
+   apply(force simp add: fresh_prod fresh_fun_simp_OrL calc_atm)
+  by (meson exists_fresh(1) fs_name1)
 
 lemma fresh_fun_simp_ImpL:
   assumes a: "z'\<sharp>P" "z'\<sharp>M" "z'\<sharp>N" "z'\<sharp>x"
   shows "fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.M (x).N z') = Cut <c>.P (z').ImpL <a>.M (x).N z'"
-using a
-apply -
-apply(rule fresh_fun_app)
-apply(rule pt_name_inst)
-apply(rule at_name_inst)
-apply(finite_guess)
-apply(subgoal_tac "\<exists>n::name. n\<sharp>(c,P,x,M,N)")
-apply(erule exE)
-apply(rule_tac x="n" in exI)
-apply(simp add: fresh_prod abs_fresh)
-apply(fresh_guess)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(fresh_guess)
-done
+proof (rule fresh_fun_app [OF pt_name_inst at_name_inst])
+  obtain n::name where "n\<sharp>(c,P,x,M,N)"
+    by (meson exists_fresh(1) fs_name1)
+  then show "\<exists>aa. aa \<sharp> (\<lambda>z'. Cut <c>.P(z').ImpL <a>.M(x).N z', Cut <c>.P(aa).ImpL <a>.M(x).N aa)"
+    apply(intro exI [where x="n"])
+    apply(simp add: fresh_prod abs_fresh)
+    apply(fresh_guess)
+    done
+next
+  show "z' \<sharp> (\<lambda>z'. Cut <c>.P(z').ImpL <a>.M(x).N z')"
+    using a by(fresh_guess) 
+qed finite_guess
 
 lemma fresh_fun_ImpL[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
   shows "pi1\<bullet>fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.M (x).N z')=
              fresh_fun (pi1\<bullet>(\<lambda>z'. Cut <c>.P (z').ImpL <a>.M (x).N z'))"
   and   "pi2\<bullet>fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.M (x).N z')=
              fresh_fun (pi2\<bullet>(\<lambda>z'. Cut <c>.P (z').ImpL <a>.M (x).N z'))"
-apply -
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,N,x,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>N,pi1\<bullet>x,pi1)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_ImpL at_prm_fresh[OF at_name_inst] swap_simps)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,N,x,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>N,pi2\<bullet>x,pi2)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_ImpL calc_atm)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-done
+   apply(perm_simp)
+   apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,N,x,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>N,pi1\<bullet>x,pi1)")
+    apply(force simp add: fresh_prod fresh_fun_simp_ImpL at_prm_fresh[OF at_name_inst] swap_simps)
+   apply (meson exists_fresh(1) fs_name1)
+  apply(perm_simp)
+  apply(subgoal_tac "\<exists>n::name. n\<sharp>(P,M,N,x,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>N,pi2\<bullet>x,pi2)")
+   apply(force simp add: fresh_prod fresh_fun_simp_ImpL calc_atm)
+  by (meson exists_fresh(1) fs_name1)
 
 lemma fresh_fun_simp_NotR:
   assumes a: "a'\<sharp>P" "a'\<sharp>M"
   shows "fresh_fun (\<lambda>a'. Cut <a'>.(NotR (y).M a') (x).P) = Cut <a'>.(NotR (y).M a') (x).P"
-using a
-apply -
-apply(rule fresh_fun_app)
-apply(rule pt_coname_inst)
-apply(rule at_coname_inst)
-apply(finite_guess)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(x,P,y,M)")
-apply(erule exE)
-apply(rule_tac x="n" in exI)
-apply(simp add: fresh_prod abs_fresh)
-apply(fresh_guess)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(fresh_guess)
-done
+proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
+  obtain n::coname where "n\<sharp>(x,P,y,M)"
+    by (metis assms(1) assms(2) fresh_atm(4) fresh_prod)
+  then show "\<exists>a. a \<sharp> (\<lambda>a'. Cut <a'>.(NotR (y).M a') (x).P, Cut <a>.NotR(y).M(a) (x).P)"
+    apply(intro exI [where x="n"])
+    apply(simp add: fresh_prod abs_fresh)
+    apply(fresh_guess)
+    done
+qed (use a in \<open>fresh_guess|finite_guess\<close>)+
 
 lemma fresh_fun_NotR[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
   shows "pi1\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(NotR (y).M a') (x).P)=
              fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(NotR (y).M a') (x).P))"
   and   "pi2\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(NotR (y).M a') (x).P)=
              fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(NotR (y).M a') (x).P))"
-apply -
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,pi1\<bullet>P,pi1\<bullet>M,pi1)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_NotR calc_atm)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,pi2\<bullet>P,pi2\<bullet>M,pi2)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_NotR at_prm_fresh[OF at_coname_inst] swap_simps)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-done
+   apply(perm_simp)
+   apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,pi1\<bullet>P,pi1\<bullet>M,pi1)")
+    apply(force simp add: fresh_prod fresh_fun_simp_NotR calc_atm)
+   apply (meson exists_fresh(2) fs_coname1)
+  apply(perm_simp)
+  apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,pi2\<bullet>P,pi2\<bullet>M,pi2)")
+   apply(force simp: fresh_prod fresh_fun_simp_NotR at_prm_fresh[OF at_coname_inst] swap_simps)
+  by (meson exists_fresh(2) fs_coname1)
 
 lemma fresh_fun_simp_AndR:
   assumes a: "a'\<sharp>P" "a'\<sharp>M" "a'\<sharp>N" "a'\<sharp>b" "a'\<sharp>c"
   shows "fresh_fun (\<lambda>a'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P) = Cut <a'>.(AndR <b>.M <c>.N a') (x).P"
-using a
-apply -
-apply(rule fresh_fun_app)
-apply(rule pt_coname_inst)
-apply(rule at_coname_inst)
-apply(finite_guess)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(x,P,b,M,c,N)")
-apply(erule exE)
-apply(rule_tac x="n" in exI)
-apply(simp add: fresh_prod abs_fresh)
-apply(fresh_guess)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(fresh_guess)
-done
+proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
+  obtain n::coname where "n\<sharp>(x,P,b,M,c,N)"
+    by (meson exists_fresh(2) fs_coname1)
+  then show "\<exists>a. a \<sharp> (\<lambda>a'. Cut <a'>.AndR <b>.M <c>.N(a') (x).P, Cut <a>.AndR <b>.M <c>.N(a) (x).P)"
+    apply(intro exI [where x="n"])
+    apply(simp add: fresh_prod abs_fresh)
+    apply(fresh_guess)
+    done
+qed (use a in \<open>fresh_guess|finite_guess\<close>)+
 
 lemma fresh_fun_AndR[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
   shows "pi1\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P)=
              fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P))"
   and   "pi2\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P)=
              fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(AndR <b>.M <c>.N a') (x).P))"
-apply -
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,N,b,c,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>N,pi1\<bullet>b,pi1\<bullet>c,pi1)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_AndR calc_atm)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,N,b,c,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>N,pi2\<bullet>b,pi2\<bullet>c,pi2)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_AndR at_prm_fresh[OF at_coname_inst] swap_simps)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-done
+   apply(perm_simp)
+   apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,N,b,c,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>N,pi1\<bullet>b,pi1\<bullet>c,pi1)")
+    apply(force simp add: fresh_prod fresh_fun_simp_AndR calc_atm)
+   apply (meson exists_fresh(2) fs_coname1)
+  apply(perm_simp)
+  apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,N,b,c,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>N,pi2\<bullet>b,pi2\<bullet>c,pi2)")
+   apply(force simp add: fresh_prod fresh_fun_simp_AndR at_prm_fresh[OF at_coname_inst] swap_simps)
+  by (meson exists_fresh(2) fs_coname1)
 
 lemma fresh_fun_simp_OrR1:
   assumes a: "a'\<sharp>P" "a'\<sharp>M" "a'\<sharp>b" 
   shows "fresh_fun (\<lambda>a'. Cut <a'>.(OrR1 <b>.M a') (x).P) = Cut <a'>.(OrR1 <b>.M a') (x).P"
-using a
-apply -
-apply(rule fresh_fun_app)
-apply(rule pt_coname_inst)
-apply(rule at_coname_inst)
-apply(finite_guess)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(x,P,b,M)")
-apply(erule exE)
-apply(rule_tac x="n" in exI)
-apply(simp add: fresh_prod abs_fresh)
-apply(fresh_guess)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(fresh_guess)
-done
+proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
+  obtain n::coname where "n\<sharp>(x,P,b,M)"
+    by (meson exists_fresh(2) fs_coname1)
+  then show "\<exists>a. a \<sharp> (\<lambda>a'. Cut <a'>.OrR1 <b>.M(a') (x).P, Cut <a>.OrR1 <b>.M(a) (x).P)"
+    apply(intro exI [where x="n"])
+    apply(simp add: fresh_prod abs_fresh)
+    apply(fresh_guess)
+    done
+qed (use a in \<open>fresh_guess|finite_guess\<close>)+
 
 lemma fresh_fun_OrR1[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
   shows "pi1\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(OrR1 <b>.M a') (x).P)=
              fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(OrR1 <b>.M  a') (x).P))"
   and   "pi2\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(OrR1 <b>.M a') (x).P)=
              fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(OrR1 <b>.M a') (x).P))"
-apply -
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>b,pi1)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_OrR1 calc_atm)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_OrR1 at_prm_fresh[OF at_coname_inst] swap_simps)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-done
+   apply(perm_simp)
+   apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>b,pi1)")
+    apply(force simp add: fresh_prod fresh_fun_simp_OrR1 calc_atm)
+   apply (meson exists_fresh(2) fs_coname1)
+  apply(perm_simp)
+  apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)")
+   apply(force simp add: fresh_prod fresh_fun_simp_OrR1 at_prm_fresh[OF at_coname_inst] swap_simps)
+  by (meson exists_fresh(2) fs_coname1)
 
 lemma fresh_fun_simp_OrR2:
   assumes a: "a'\<sharp>P" "a'\<sharp>M" "a'\<sharp>b" 
   shows "fresh_fun (\<lambda>a'. Cut <a'>.(OrR2 <b>.M a') (x).P) = Cut <a'>.(OrR2 <b>.M a') (x).P"
-using a
-apply -
-apply(rule fresh_fun_app)
-apply(rule pt_coname_inst)
-apply(rule at_coname_inst)
-apply(finite_guess)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(x,P,b,M)")
-apply(erule exE)
-apply(rule_tac x="n" in exI)
-apply(simp add: fresh_prod abs_fresh)
-apply(fresh_guess)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(fresh_guess)
-done
+proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
+  obtain n::coname where "n\<sharp>(x,P,b,M)"
+    by (meson exists_fresh(2) fs_coname1)
+  then show "\<exists>a. a \<sharp> (\<lambda>a'. Cut <a'>.OrR2 <b>.M(a') (x).P, Cut <a>.OrR2 <b>.M(a) (x).P)"
+    apply(intro exI [where x="n"])
+    apply(simp add: fresh_prod abs_fresh)
+    apply(fresh_guess)
+    done
+qed (use a in \<open>fresh_guess|finite_guess\<close>)+
 
 lemma fresh_fun_OrR2[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
   shows "pi1\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(OrR2 <b>.M a') (x).P)=
              fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(OrR2 <b>.M  a') (x).P))"
   and   "pi2\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(OrR2 <b>.M a') (x).P)=
              fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(OrR2 <b>.M a') (x).P))"
-apply -
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>b,pi1)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_OrR2 calc_atm)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_OrR2 at_prm_fresh[OF at_coname_inst] swap_simps)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-done
+   apply(perm_simp)
+   apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>b,pi1)")
+    apply(force simp add: fresh_prod fresh_fun_simp_OrR2 calc_atm)
+   apply (meson exists_fresh(2) fs_coname1)
+  apply(perm_simp)
+  apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)")
+   apply(force simp add: fresh_prod fresh_fun_simp_OrR2 at_prm_fresh[OF at_coname_inst] swap_simps)
+  by (meson exists_fresh(2) fs_coname1)
 
 lemma fresh_fun_simp_ImpR:
   assumes a: "a'\<sharp>P" "a'\<sharp>M" "a'\<sharp>b" 
   shows "fresh_fun (\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M a') (x).P) = Cut <a'>.(ImpR (y).<b>.M a') (x).P"
-using a
-apply -
-apply(rule fresh_fun_app)
-apply(rule pt_coname_inst)
-apply(rule at_coname_inst)
-apply(finite_guess)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(x,P,y,b,M)")
-apply(erule exE)
-apply(rule_tac x="n" in exI)
-apply(simp add: fresh_prod abs_fresh)
-apply(fresh_guess)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(fresh_guess)
-done
+proof (rule fresh_fun_app [OF pt_coname_inst at_coname_inst])
+  obtain n::coname where "n\<sharp>(x,P,y,b,M)"
+    by (meson exists_fresh(2) fs_coname1)
+  then show "\<exists>a. a \<sharp> (\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M a') (x).P, Cut <a>.(ImpR (y).<b>.M a) (x).P)"
+    apply(intro exI [where x="n"])
+    apply(simp add: fresh_prod abs_fresh)
+    apply(fresh_guess)
+    done
+qed (use a in \<open>fresh_guess|finite_guess\<close>)+
 
 lemma fresh_fun_ImpR[eqvt_force]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
   shows "pi1\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M a') (x).P)=
              fresh_fun (pi1\<bullet>(\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M  a') (x).P))"
   and   "pi2\<bullet>fresh_fun (\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M a') (x).P)=
              fresh_fun (pi2\<bullet>(\<lambda>a'. Cut <a'>.(ImpR (y).<b>.M a') (x).P))"
-apply -
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>b,pi1)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_ImpR calc_atm)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-apply(perm_simp)
-apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)")
-apply(simp add: fresh_prod)
-apply(auto)
-apply(simp add: fresh_fun_simp_ImpR at_prm_fresh[OF at_coname_inst] swap_simps)
-apply(rule exists_fresh')
-apply(simp add: fin_supp)
-done
+   apply(perm_simp)
+   apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi1\<bullet>P,pi1\<bullet>M,pi1\<bullet>b,pi1)")
+    apply(force simp add: fresh_prod fresh_fun_simp_ImpR calc_atm)
+   apply (meson exists_fresh(2) fs_coname1)
+  apply(perm_simp)
+  apply(subgoal_tac "\<exists>n::coname. n\<sharp>(P,M,b,pi2\<bullet>P,pi2\<bullet>M,pi2\<bullet>b,pi2)")
+   apply(force simp add: fresh_prod fresh_fun_simp_ImpR at_prm_fresh[OF at_coname_inst] swap_simps)
+  by (meson exists_fresh(2) fs_coname1)
 
 nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)")
   substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) 
 where
   "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" 

    else OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z)"
 | "\<lbrakk>a\<sharp>(b,c,P); x\<sharp>(y,P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){y:=<c>.P} = ImpR (x).<a>.(M{y:=<c>.P}) b"
 | "\<lbrakk>a\<sharp>(N,c,P);x\<sharp>(y,P,M,z)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = 
   (if y=z then fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z') 
    else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"
-apply(finite_guess)+
-apply(rule TrueI)+
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::name. x\<sharp>(x1,P,y1)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::name. x\<sharp>(x1,P,y1)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::name. x\<sharp>(x1,P,y1)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::name. x\<sharp>(x1,P,y1,x3,y2)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::name. x\<sharp>(x1,P,y1,x3,y2)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrL abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::name. x\<sharp>(x3,P,y1,y2)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::name. x\<sharp>(x3,P,y1,y2)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpL abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
+apply(finite_guess | simp add: abs_fresh abs_supp fin_supp | fresh_guess | rule strip)+
+apply(subgoal_tac "\<exists>x::name. x\<sharp>(x1,P,y1)")
+apply(force simp add: fresh_prod fresh_fun_simp_NotL abs_fresh fresh_atm)
+apply (meson exists_fresh(1) fs_name1)
+
+apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
+apply(subgoal_tac "\<exists>x::name. x\<sharp>(x1,P,y1)")
+apply(force simp add: fresh_prod fresh_fun_simp_AndL1 abs_fresh fresh_atm)
+apply (meson exists_fresh(1) fs_name1)
+
+apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
+apply(subgoal_tac "\<exists>x::name. x\<sharp>(x1,P,y1)")
+apply(force simp add: fresh_prod fresh_fun_simp_AndL2 abs_fresh fresh_atm)
+apply (meson exists_fresh(1) fs_name1)
+
+apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
+apply(subgoal_tac "\<exists>x::name. x\<sharp>(x1,P,y1,x3,y2)")
+apply(force simp add: fresh_prod fresh_fun_simp_OrL abs_fresh fresh_atm)
+apply (meson exists_fresh(1) fs_name1)
+
+apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
+apply(subgoal_tac "\<exists>x::name. x\<sharp>(x1,P,y1,x3,y2)")
+apply(force simp add: fresh_prod fresh_fun_simp_OrL abs_fresh fresh_atm)
+apply (meson exists_fresh(1) fs_name1)
+
+apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
+apply(subgoal_tac "\<exists>x::name. x\<sharp>(x3,P,y1,y2)")
+apply(force simp add: fresh_prod fresh_fun_simp_ImpL abs_fresh fresh_atm)
+apply (meson exists_fresh(1) fs_name1)
+
+apply(simp add: abs_fresh abs_supp fin_supp | rule strip)+
+apply(subgoal_tac "\<exists>x::name. x\<sharp>(x3,P,y1,y2)")
+apply(force simp add: fresh_prod fresh_fun_simp_ImpL abs_fresh fresh_atm)
+apply (meson exists_fresh(1) fs_name1)
 apply(fresh_guess)+
 done
 
 nominal_primrec (freshness_context: "(d::name,z::coname,P::trm)")
   substc :: "trm \<Rightarrow> coname \<Rightarrow> name   \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=(_)._}" [100,100,100,100] 100)

 | "\<lbrakk>a\<sharp>(b,d,P); x\<sharp>(z,P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){d:=(z).P} = 
   (if d=b then fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.(M{d:=(z).P}) a' (z).P) 
    else ImpR (x).<a>.(M{d:=(z).P}) b)"
 | "\<lbrakk>a\<sharp>(N,d,P);x\<sharp>(y,z,P,M)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y){d:=(z).P} = 
   ImpL <a>.(M{d:=(z).P}) (x).(N{d:=(z).P}) y"
-apply(finite_guess)+
-apply(rule TrueI)+
-apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,y1)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,y1,x3,y2)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,y1,x3,y2)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_AndR abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,y1)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrR1 abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,y1)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_OrR2 abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,x2,y1)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpR abs_fresh fresh_atm abs_supp)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(rule impI)
-apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,x2,y1)", erule exE, simp add: fresh_prod)
-apply(erule conjE)+
-apply(simp add: fresh_fun_simp_ImpR abs_fresh fresh_atm)
-apply(rule exists_fresh', simp add: fin_supp)
-apply(simp add: abs_fresh abs_supp)+
-apply(fresh_guess add: abs_fresh fresh_prod)+
-done
+apply(finite_guess | simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
+apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,y1)")
+apply(force simp add: fresh_prod fresh_fun_simp_NotR abs_fresh fresh_atm)
+apply(meson exists_fresh' fin_supp)
+
+apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
+apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,y1,x3,y2)")
+apply(force simp add: fresh_prod fresh_fun_simp_AndR abs_fresh fresh_atm)
+apply(meson exists_fresh' fin_supp)
+
+apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
+apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,y1,x3,y2)")
+apply(force simp add: fresh_prod fresh_fun_simp_AndR abs_fresh fresh_atm)
+apply(meson exists_fresh' fin_supp)
+
+apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
+apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,y1)")
+apply(force simp add: fresh_prod fresh_fun_simp_OrR1 abs_fresh fresh_atm)
+apply(meson exists_fresh' fin_supp)
+
+apply(simp add: abs_fresh abs_supp fs_name1 fs_coname1 | rule strip)+
+apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,y1)")
+apply(force simp add: fresh_prod fresh_fun_simp_OrR2 abs_fresh fresh_atm)
+apply(meson exists_fresh' fin_supp)
+
+apply(simp add: abs_fresh abs_supp | rule strip)+
+apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,x2,y1)")
+apply(force simp add: fresh_prod fresh_fun_simp_ImpR abs_fresh fresh_atm abs_supp)
+apply(meson exists_fresh' fin_supp)
+
+apply(simp add: abs_fresh abs_supp | rule strip)+
+apply(subgoal_tac "\<exists>x::coname. x\<sharp>(x1,P,x2,y1)")
+apply(force simp add: fresh_prod fresh_fun_simp_ImpR abs_fresh fresh_atm)
+apply(meson exists_fresh' fin_supp)
+
+apply(simp add: abs_fresh | fresh_guess add: abs_fresh)+
+done
+
 
 lemma csubst_eqvt[eqvt]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
   shows "pi1\<bullet>(M{c:=(x).N}) = (pi1\<bullet>M){(pi1\<bullet>c):=(pi1\<bullet>x).(pi1\<bullet>N)}"
   and   "pi2\<bullet>(M{c:=(x).N}) = (pi2\<bullet>M){(pi2\<bullet>c):=(pi2\<bullet>x).(pi2\<bullet>N)}"
 apply(nominal_induct M avoiding: c x N rule: trm.strong_induct)
-apply(auto simp add: eq_bij fresh_bij eqvts)
+apply(auto simp: eq_bij fresh_bij eqvts)
 apply(perm_simp)+
 done
 
 lemma nsubst_eqvt[eqvt]:
   fixes pi1::"name prm"
   and   pi2::"coname prm"
   shows "pi1\<bullet>(M{x:=<c>.N}) = (pi1\<bullet>M){(pi1\<bullet>x):=<(pi1\<bullet>c)>.(pi1\<bullet>N)}"
   and   "pi2\<bullet>(M{x:=<c>.N}) = (pi2\<bullet>M){(pi2\<bullet>x):=<(pi2\<bullet>c)>.(pi2\<bullet>N)}"
 apply(nominal_induct M avoiding: c x N rule: trm.strong_induct)
-apply(auto simp add: eq_bij fresh_bij eqvts)
+apply(auto simp: eq_bij fresh_bij eqvts)
 apply(perm_simp)+
 done
 
 lemma supp_subst1:
   shows "supp (M{y:=<c>.P}) \<subseteq> ((supp M) - {y}) \<union> (supp P)"
 apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
 apply(auto)
-apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
+apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
 apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{y:=<c>.P},P)")
 apply(erule exE)
 apply(simp add: fresh_prod)
 apply(erule conjE)+

 
 lemma supp_subst2:
   shows "supp (M{y:=<c>.P}) \<subseteq> supp (M) \<union> ((supp P) - {c})"
 apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
 apply(auto)
-apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
+apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
 apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{y:=<c>.P},P)")
 apply(erule exE)
 apply(simp add: fresh_prod)
 apply(erule conjE)+

 
 lemma supp_subst3:
   shows "supp (M{c:=(x).P}) \<subseteq> ((supp M) - {c}) \<union> (supp P)"
 apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
 apply(auto)
-apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
+apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
 apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname:=(x).P},P)")
 apply(erule exE)
 apply(simp add: fresh_prod)
 apply(erule conjE)+

 
 lemma supp_subst4:
   shows "supp (M{c:=(x).P}) \<subseteq> (supp M) \<union> ((supp P) - {x})"
 apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
 apply(auto)
-apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
+apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
 apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname:=(x).P},P)")
 apply(erule exE)
 apply(simp add: fresh_prod)
 apply(erule conjE)+

 
 lemma supp_subst5:
   shows "(supp M - {y}) \<subseteq> supp (M{y:=<c>.P})"
 apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
 apply(auto)
-apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
+apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
 apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{y:=<c>.P},P)")
 apply(erule exE)
 apply(simp add: fresh_prod)
 apply(erule conjE)+

 
 lemma supp_subst6:
   shows "(supp M) \<subseteq> ((supp (M{y:=<c>.P}))::coname set)"
 apply(nominal_induct M avoiding: y P c rule: trm.strong_induct)
 apply(auto)
-apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
+apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
 apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{y:=<c>.P},P)")
 apply(erule exE)
 apply(simp add: fresh_prod)
 apply(erule conjE)+

 
 lemma supp_subst7:
   shows "(supp M - {c}) \<subseteq>  supp (M{c:=(x).P})"
 apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
 apply(auto)
-apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
+apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
 apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname:=(x).P},P)")
 apply(erule exE)
 apply(simp add: fresh_prod)
 apply(erule conjE)+

 
 lemma supp_subst8:
   shows "(supp M) \<subseteq> ((supp (M{c:=(x).P}))::name set)"
 apply(nominal_induct M avoiding: x P c rule: trm.strong_induct)
 apply(auto)
-apply(auto simp add: fresh_def abs_supp trm.supp supp_atm fin_supp)
+apply(auto simp: fresh_def abs_supp trm.supp supp_atm fin_supp)
 apply(blast)+
 apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname:=(x).P},P)")
 apply(erule exE)
 apply(simp add: fresh_prod)
 apply(erule conjE)+

 
 lemma forget:
   shows "x\<sharp>M \<Longrightarrow> M{x:=<c>.P} = M"
   and   "c\<sharp>M \<Longrightarrow> M{c:=(x).P} = M"
 apply(nominal_induct M avoiding: x c P rule: trm.strong_induct)
-apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
+apply(auto simp: fresh_atm abs_fresh abs_supp fin_supp)
 done
 
 lemma substc_rename1:
   assumes a: "c\<sharp>(M,a)"
   shows "M{a:=(x).N} = ([(c,a)]\<bullet>M){c:=(x).N}"
 using a
 proof(nominal_induct M avoiding: c a x N rule: trm.strong_induct)
   case (Ax z d)
-  then show ?case by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha)
+  then show ?case by (auto simp: fresh_prod fresh_atm calc_atm trm.inject alpha)
 next
   case NotL
-  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
+  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (NotR y M d)
   then show ?case 
-    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
+    by(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (AndR c1 M c2 M' c3)
   then show ?case
-    apply(auto simp add: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
+    apply(auto simp: fresh_prod calc_atm fresh_atm abs_fresh fresh_left)
     apply (metis (erased, opaque_lifting))
     by metis
 next
   case AndL1
-  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
+  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case AndL2
-  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
+  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (OrR1 d M e)
   then show ?case 
-    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
+    by(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (OrR2 d M e)
   then show ?case 
-    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
+    by(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (OrL x1 M x2 M' x3)
   then show ?case
-    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
 next 
   case ImpL
   then show ?case
-    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
        metis
 next
   case (ImpR y d M e)
   then show ?case
-    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    by(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
 next
   case (Cut d M y M')
   then show ?case
     by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
       (metis crename.simps(1) crename_id crename_rename)

   shows "M{a:=(x).N} = M{a:=(y).([(y,x)]\<bullet>N)}"
 using a
 proof(nominal_induct M avoiding: a x y N rule: trm.strong_induct)
   case (Ax z d)
   then show ?case 
-    by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
+    by (auto simp: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
 next
   case NotL
   then show ?case 
-    by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
+    by (auto simp: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
 next
   case (NotR y M d)
   then show ?case
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{d:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>N)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_NotR)
     apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (AndR c1 M c2 M' c3)
   then show ?case
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
     apply(subgoal_tac 
        "\<exists>a'::coname. a'\<sharp>(N,M{c3:=(y).([(y,x)]\<bullet>N)},M'{c3:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>N,c1,c2,c3)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndR)
-    apply (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh subst_fresh perm_swap fresh_left)
+    apply (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh subst_fresh perm_swap fresh_left)
     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case AndL1
-  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
 next
   case AndL2
-  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
 next
   case (OrR1 d M e)
   then show ?case 
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>N,d,e)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_OrR1)
     apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (OrR2 d M e)
   then show ?case
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>N,d,e)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_OrR2)
     apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (OrL x1 M x2 M' x3)
   then show ?case
-    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
 next 
   case ImpL
   then show ?case
-    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
 next
   case (ImpR y d M e)
   then show ?case
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(N,M{e:=(y).([(y,x)]\<bullet>N)},[(y,x)]\<bullet>N,d,e)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_ImpR)
     apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (Cut d M y M')
   then show ?case
-    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left perm_swap)
+    by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left perm_swap)
 qed
 
 lemma substn_rename3:
   assumes a: "y\<sharp>(M,x)"
   shows "M{x:=<a>.N} = ([(y,x)]\<bullet>M){y:=<a>.N}"
 using a
 proof(nominal_induct M avoiding: a x y N rule: trm.strong_induct)
   case (Ax z d)
-  then show ?case by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha)
+  then show ?case by (auto simp: fresh_prod fresh_atm calc_atm trm.inject alpha)
 next
   case NotR
-  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
+  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (NotL d M z)
   then show ?case 
-    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
+    by(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (AndR c1 M c2 M' c3)
   then show ?case
-    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
 next
   case OrR1
-  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
+  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case OrR2
-  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
+  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (AndL1 u M v)
   then show ?case 
-    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
+    by(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (AndL2 u M v)
   then show ?case 
-    by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
+    by(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod)
 next
   case (OrL x1 M x2 M' x3)
   then show ?case
     by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
       (metis (poly_guards_query))
 next 
   case ImpR
   then show ?case
-  by(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_left abs_supp fin_supp fresh_prod)
+  by(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_left abs_supp fin_supp fresh_prod)
 next
   case (ImpL d M v M' u)
   then show ?case
     by(simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
        (metis (poly_guards_query))
 next
   case (Cut d M y M')
   then show ?case
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
     apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
     apply(simp add: calc_atm)
     apply metis
     done
 qed

   shows "M{x:=<a>.N} = M{x:=<c>.([(c,a)]\<bullet>N)}"
 using a
 proof(nominal_induct M avoiding: x c a N rule: trm.strong_induct)
   case (Ax z d)
   then show ?case 
-    by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
+    by (auto simp: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
 next
   case NotR
   then show ?case 
-    by (auto simp add: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
+    by (auto simp: fresh_prod fresh_atm calc_atm trm.inject alpha perm_swap fresh_left)
 next
   case (NotL d M y)
   then show ?case
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
     apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{x:=<c>.([(c,a)]\<bullet>N)},[(c,a)]\<bullet>N)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_NotL)
     apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (OrL x1 M x2 M' x3)
   then show ?case
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
     apply(subgoal_tac 
        "\<exists>a'::name. a'\<sharp>(N,M{x:=<c>.([(c,a)]\<bullet>N)},M'{x:=<c>.([(c,a)]\<bullet>N)},[(c,a)]\<bullet>N,x1,x2,x3)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_OrL)
-    apply (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh subst_fresh perm_swap fresh_left)
+    apply (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh subst_fresh perm_swap fresh_left)
     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case OrR1
-  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
 next
   case OrR2
-  then show ?case by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+  then show ?case by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
 next
   case (AndL1 u M v)
   then show ?case 
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
     apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{x:=<c>.([(c,a)]\<bullet>N)},[(c,a)]\<bullet>N,u,v)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndL1)
     apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (AndL2 u M v)
   then show ?case 
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
     apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{x:=<c>.([(c,a)]\<bullet>N)},[(c,a)]\<bullet>N,u,v)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndL2)
     apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (AndR c1 M c2 M' c3)
   then show ?case
-    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
 next 
   case ImpR
   then show ?case
-    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
 next
   case (ImpL d M y M' u)
   then show ?case
-    apply(auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
+    apply(auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left)
     apply(subgoal_tac "\<exists>a'::name. a'\<sharp>(N,M{u:=<c>.([(c,a)]\<bullet>N)},M'{u:=<c>.([(c,a)]\<bullet>N)},[(c,a)]\<bullet>N,y,u)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_ImpL)
     apply(simp add: trm.inject alpha perm_swap fresh_left calc_atm)
     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (Cut d M y M')
   then show ?case
-    by (auto simp add: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left perm_swap)
+    by (auto simp: calc_atm trm.inject alpha fresh_atm abs_fresh fresh_prod fresh_left perm_swap)
 qed
 
 lemma subst_rename5:
   assumes a: "c'\<sharp>(c,N)" "x'\<sharp>(x,M)"
   shows "M{x:=<c>.N} = ([(x',x)]\<bullet>M){x':=<c'>.([(c',c)]\<bullet>N)}"

   (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))"
 proof -   
   obtain x'::"name"   where fs1: "x'\<sharp>(M,N,c,P,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(M,N,c,P,a)" by (rule exists_fresh(2), rule fin_supp, blast)
   have eq1: "(Cut <a>.M (x).N) = (Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N))"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   have eq2: "(M=Ax y a) = (([(a',a)]\<bullet>M)=Ax y a')"
-    apply(auto simp add: calc_atm)
+    apply(auto simp: calc_atm)
     apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
     apply(simp add: calc_atm)
     done
   have "(Cut <a>.M (x).N){y:=<c>.P} = (Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N)){y:=<c>.P}" 
     using eq1 by simp
   also have "\<dots> = (if ([(a',a)]\<bullet>M)=Ax y a' then Cut <c>.P (x').(([(x',x)]\<bullet>N){y:=<c>.P}) 
                               else Cut <a'>.(([(a',a)]\<bullet>M){y:=<c>.P}) (x').(([(x',x)]\<bullet>N){y:=<c>.P}))" 
-    using fs1 fs2 by (auto simp add: fresh_prod fresh_left calc_atm fresh_atm)
+    using fs1 fs2 by (auto simp: fresh_prod fresh_left calc_atm fresh_atm)
   also have "\<dots> =(if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))"
     using fs1 fs2 a
     apply -
     apply(simp only: eq2[symmetric])
-    apply(auto simp add: trm.inject)
+    apply(auto simp: trm.inject)
     apply(simp_all add: alpha fresh_atm fresh_prod subst_fresh)
     apply(simp_all add: eqvts perm_fresh_fresh calc_atm)
     apply(auto)
     apply(rule subst_rename)
     apply(simp add: fresh_prod fresh_atm)

   (if N=Ax x c then Cut <a>.(M{c:=(y).P}) (y).P else Cut <a>.(M{c:=(y).P}) (x).(N{c:=(y).P}))" 
 proof -   
   obtain x'::"name"   where fs1: "x'\<sharp>(M,N,c,P,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(M,N,c,P,a)" by (rule exists_fresh(2), rule fin_supp, blast)
   have eq1: "(Cut <a>.M (x).N) = (Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N))"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   have eq2: "(N=Ax x c) = (([(x',x)]\<bullet>N)=Ax x' c)"
-    apply(auto simp add: calc_atm)
+    apply(auto simp: calc_atm)
     apply(drule pt_bij1[OF pt_name_inst, OF at_name_inst])
     apply(simp add: calc_atm)
     done
   have "(Cut <a>.M (x).N){c:=(y).P} = (Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N)){c:=(y).P}" 
     using eq1 by simp

     using fs1 fs2  by (simp add: fresh_prod fresh_left calc_atm fresh_atm trm.inject)
   also have "\<dots> =(if N=Ax x c then Cut <a>.(M{c:=(y).P}) (y).P else Cut <a>.(M{c:=(y).P}) (x).(N{c:=(y).P}))"
     using fs1 fs2 a
     apply -
     apply(simp only: eq2[symmetric])
-    apply(auto simp add: trm.inject)
+    apply(auto simp: trm.inject)
     apply(simp_all add: alpha fresh_atm fresh_prod subst_fresh)
     apply(simp_all add: eqvts perm_fresh_fresh calc_atm)
     apply(auto)
     apply(rule subst_rename)
     apply(simp add: fresh_prod fresh_atm)

 apply(subgoal_tac "Cut <a>.M (x).N = Cut <a>.M (ca).([(ca,x)]\<bullet>N)")
 apply(simp)
 apply(subgoal_tac"y\<sharp>([(ca,x)]\<bullet>N)")
 apply(simp add: forget)
 apply(simp add: trm.inject)
-apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
+apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1]
 apply(simp add: trm.inject)
 apply(rule sym)
 apply(simp add: alpha fresh_prod fresh_atm)
 done
 

   shows "(NotR (x).M d){d:=(z).P} = fresh_fun (\<lambda>a'. Cut <a'>.NotR (x).M a' (z).P)"
 using a
 apply -
 apply(generate_fresh "name")
 apply(subgoal_tac "NotR (x).M d = NotR (c).([(c,x)]\<bullet>M) d")
-apply(auto simp add: fresh_left calc_atm forget)
+apply(auto simp: fresh_left calc_atm forget)
 apply(generate_fresh "coname")
 apply(rule_tac f="fresh_fun" in arg_cong)
 apply(simp add:  fun_eq_iff)
 apply(rule allI)
 apply(simp add: trm.inject alpha fresh_prod fresh_atm)

   shows "(NotL <a>.M y){y:=<c>.P} = fresh_fun (\<lambda>x'. Cut <c>.P (x').NotL <a>.M x')"
 using a
 apply -
 apply(generate_fresh "coname")
 apply(subgoal_tac "NotL <a>.M y = NotL <ca>.([(ca,a)]\<bullet>M) y")
-apply(auto simp add: fresh_left calc_atm forget)
+apply(auto simp: fresh_left calc_atm forget)
 apply(generate_fresh "name")
 apply(rule_tac f="fresh_fun" in arg_cong)
 apply(simp add:  fun_eq_iff)
 apply(rule allI)
 apply(simp add: trm.inject alpha fresh_prod fresh_atm)

   shows "(AndL1 (x).M y){y:=<c>.P} = fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).M z')"
 using a
 apply -
 apply(generate_fresh "name")
 apply(subgoal_tac "AndL1 (x).M y = AndL1 (ca).([(ca,x)]\<bullet>M) y")
-apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
+apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
 apply(generate_fresh "name")
 apply(rule_tac f="fresh_fun" in arg_cong)
 apply(simp add:  fun_eq_iff)
 apply(rule allI)
 apply(simp add: trm.inject alpha fresh_prod fresh_atm)

   shows "(AndL2 (x).M y){y:=<c>.P} = fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).M z')"
 using a
 apply -
 apply(generate_fresh "name")
 apply(subgoal_tac "AndL2 (x).M y = AndL2 (ca).([(ca,x)]\<bullet>M) y")
-apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
+apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
 apply(generate_fresh "name")
 apply(rule_tac f="fresh_fun" in arg_cong)
 apply(simp add:  fun_eq_iff)
 apply(rule allI)
 apply(simp add: trm.inject alpha fresh_prod fresh_atm)

 using a
 apply -
 apply(generate_fresh "coname")
 apply(generate_fresh "coname")
 apply(subgoal_tac "AndR <a>.M <b>.N c = AndR <ca>.([(ca,a)]\<bullet>M) <caa>.([(caa,b)]\<bullet>N) c")
-apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
+apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
 apply(rule trans)
 apply(rule substc.simps)
-apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
-apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
-apply(auto simp add: fresh_prod fresh_atm)[1]
+apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1]
+apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1]
+apply(auto simp: fresh_prod fresh_atm)[1]
 apply(simp)
 apply(rule_tac f="fresh_fun" in arg_cong)
 apply(simp add:  fun_eq_iff)
 apply(rule allI)
 apply(simp add: trm.inject alpha fresh_prod fresh_atm)
 apply(rule conjI)
 apply(rule forget)
-apply(auto simp add: fresh_left calc_atm abs_fresh)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh)[1]
 apply(rule forget)
-apply(auto simp add: fresh_left calc_atm abs_fresh)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh)[1]
 apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
 apply(auto)
 done
 
 lemma better_OrL_substn:

 using a
 apply -
 apply(generate_fresh "name")
 apply(generate_fresh "name")
 apply(subgoal_tac "OrL (y).M (z).N x = OrL (ca).([(ca,y)]\<bullet>M) (caa).([(caa,z)]\<bullet>N) x")
-apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
+apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
 apply(rule trans)
 apply(rule substn.simps)
-apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
-apply(auto simp add: fresh_left calc_atm fresh_prod fresh_atm)[1]
-apply(auto simp add: fresh_prod fresh_atm)[1]
+apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1]
+apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1]
+apply(auto simp: fresh_prod fresh_atm)[1]
 apply(simp)
 apply(rule_tac f="fresh_fun" in arg_cong)
 apply(simp add:  fun_eq_iff)
 apply(rule allI)
 apply(simp add: trm.inject alpha fresh_prod fresh_atm)
 apply(rule conjI)
 apply(rule forget)
-apply(auto simp add: fresh_left calc_atm abs_fresh)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh)[1]
 apply(rule forget)
-apply(auto simp add: fresh_left calc_atm abs_fresh)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh)[1]
 apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm)
 apply(auto)
 done
 
 lemma better_OrR1_substc:

   shows "(OrR1 <a>.M d){d:=(z).P} = fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.M a' (z).P)"
 using a
 apply -
 apply(generate_fresh "coname")
 apply(subgoal_tac "OrR1 <a>.M d = OrR1 <c>.([(c,a)]\<bullet>M) d")
-apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
+apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
 apply(rule_tac f="fresh_fun" in arg_cong)
 apply(simp add:  fun_eq_iff)
 apply(rule allI)
 apply(simp add: trm.inject alpha fresh_prod fresh_atm)
 apply(rule forget)

   shows "(OrR2 <a>.M d){d:=(z).P} = fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.M a' (z).P)"
 using a
 apply -
 apply(generate_fresh "coname")
 apply(subgoal_tac "OrR2 <a>.M d = OrR2 <c>.([(c,a)]\<bullet>M) d")
-apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
+apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
 apply(rule_tac f="fresh_fun" in arg_cong)
 apply(simp add:  fun_eq_iff)
 apply(rule allI)
 apply(simp add: trm.inject alpha fresh_prod fresh_atm)
 apply(rule forget)

 using a
 apply -
 apply(generate_fresh "coname")
 apply(generate_fresh "name")
 apply(subgoal_tac "ImpR (x).<a>.M d = ImpR (ca).<c>.([(c,a)]\<bullet>[(ca,x)]\<bullet>M) d")
-apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
+apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
 apply(rule_tac f="fresh_fun" in arg_cong)
 apply(simp add:  fun_eq_iff)
 apply(rule allI)
 apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm)
 apply(rule forget)

 using a
 apply -
 apply(generate_fresh "coname")
 apply(generate_fresh "name")
 apply(subgoal_tac "ImpL <a>.M (x).N y = ImpL <ca>.([(ca,a)]\<bullet>M) (caa).([(caa,x)]\<bullet>N) y")
-apply(auto simp add: fresh_left calc_atm forget abs_fresh)[1]
+apply(auto simp: fresh_left calc_atm forget abs_fresh)[1]
 apply(rule_tac f="fresh_fun" in arg_cong)
 apply(simp add:  fun_eq_iff)
 apply(rule allI)
 apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm)
 apply(rule forget)

 lemma substn_crename_comm:
   assumes a: "c\<noteq>a" "c\<noteq>b"
   shows "M{x:=<c>.P}[a\<turnstile>c>b] = M[a\<turnstile>c>b]{x:=<c>.(P[a\<turnstile>c>b])}"
 using a
 apply(nominal_induct M avoiding: x c P a b rule: trm.strong_induct)
-apply(auto simp add: subst_fresh rename_fresh trm.inject)
+apply(auto simp: subst_fresh rename_fresh trm.inject)
 apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,x,c)")
 apply(erule exE)
 apply(subgoal_tac "Cut <c>.P (x).Ax x a = Cut <c>.P (x').Ax x' a")
 apply(simp)
 apply(rule trans)

 apply(simp add: crename_id)
 apply(rule trans)
 apply(rule better_crename_Cut)
 apply(simp add: fresh_atm fresh_prod)
 apply(simp add: rename_fresh fresh_atm)
-apply(auto simp add: fresh_atm)[1]
+apply(auto simp: fresh_atm)[1]
 apply(rule trans)
 apply(rule better_crename_Cut)
 apply(simp add: fresh_atm)
-apply(auto simp add: fresh_atm)[1]
+apply(auto simp: fresh_atm)[1]
 apply(drule crename_ax)
 apply(simp add: fresh_atm)
 apply(simp add: fresh_atm)
 apply(simp)
 apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],x,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]})")

 lemma substc_crename_comm:
   assumes a: "c\<noteq>a" "c\<noteq>b"
   shows "M{c:=(x).P}[a\<turnstile>c>b] = M[a\<turnstile>c>b]{c:=(x).(P[a\<turnstile>c>b])}"
 using a
 apply(nominal_induct M avoiding: x c P a b rule: trm.strong_induct)
-apply(auto simp add: subst_fresh rename_fresh trm.inject)
+apply(auto simp: subst_fresh rename_fresh trm.inject)
 apply(rule trans)
 apply(rule better_crename_Cut)
 apply(simp add: fresh_atm fresh_prod)
 apply(simp add: rename_fresh fresh_atm)
 apply(rule trans)

 lemma substn_nrename_comm:
   assumes a: "x\<noteq>y" "x\<noteq>z"
   shows "M{x:=<c>.P}[y\<turnstile>n>z] = M[y\<turnstile>n>z]{x:=<c>.(P[y\<turnstile>n>z])}"
 using a
 apply(nominal_induct M avoiding: x c P y z rule: trm.strong_induct)
-apply(auto simp add: subst_fresh rename_fresh trm.inject)
+apply(auto simp: subst_fresh rename_fresh trm.inject)
 apply(rule trans)
 apply(rule better_nrename_Cut)
 apply(simp add: fresh_prod fresh_atm)
 apply(simp add: trm.inject)
 apply(rule trans)

 lemma substc_nrename_comm:
   assumes a: "x\<noteq>y" "x\<noteq>z"
   shows "M{c:=(x).P}[y\<turnstile>n>z] = M[y\<turnstile>n>z]{c:=(x).(P[y\<turnstile>n>z])}"
 using a
 apply(nominal_induct M avoiding: x c P y z rule: trm.strong_induct)
-apply(auto simp add: subst_fresh rename_fresh trm.inject)
+apply(auto simp: subst_fresh rename_fresh trm.inject)
 apply(rule trans)
 apply(rule better_nrename_Cut)
 apply(simp add: fresh_atm fresh_prod)
 apply(simp add: rename_fresh fresh_atm)
 apply(rule trans)

   and   x::"name"
   and   \<Gamma>::"ctxtn"
   and   \<Delta>::"ctxtc"
   shows "a\<sharp>\<Gamma>" and "x\<sharp>\<Delta>"
 proof -
-  show "a\<sharp>\<Gamma>" by (induct \<Gamma>) (auto simp add: fresh_list_nil fresh_list_cons fresh_prod fresh_atm fresh_ty)
-next
-  show "x\<sharp>\<Delta>" by (induct \<Delta>) (auto simp add: fresh_list_nil fresh_list_cons fresh_prod fresh_atm fresh_ty)
+  show "a\<sharp>\<Gamma>" by (induct \<Gamma>) (auto simp: fresh_list_nil fresh_list_cons fresh_prod fresh_atm fresh_ty)
+next
+  show "x\<sharp>\<Delta>" by (induct \<Delta>) (auto simp: fresh_list_nil fresh_list_cons fresh_prod fresh_atm fresh_ty)
 qed
 
 text \<open>cut-reductions\<close>
 
 declare abs_perm[eqvt]

 lemma fin_Ax_elim:
   assumes a: "fin (Ax x a) y"
   shows "x=y"
 using a
 apply(erule_tac fin.cases)
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 done
 
 lemma fin_NotL_elim:
   assumes a: "fin (NotL <a>.M x) y"
   shows "x=y \<and> x\<sharp>M"
 using a
 apply(erule_tac fin.cases)
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 apply(subgoal_tac "y\<sharp>[aa].Ma")
 apply(drule sym)
 apply(simp_all add: abs_fresh)
 done
 
 lemma fin_AndL1_elim:
   assumes a: "fin (AndL1 (x).M y) z"
   shows "z=y \<and> z\<sharp>[x].M"
 using a
 apply(erule_tac fin.cases)
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 done
 
 lemma fin_AndL2_elim:
   assumes a: "fin (AndL2 (x).M y) z"
   shows "z=y \<and> z\<sharp>[x].M"
 using a
 apply(erule_tac fin.cases)
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 done
 
 lemma fin_OrL_elim:
   assumes a: "fin (OrL (x).M (y).N u) z"
   shows "z=u \<and> z\<sharp>[x].M \<and> z\<sharp>[y].N"
 using a
 apply(erule_tac fin.cases)
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 done
 
 lemma fin_ImpL_elim:
   assumes a: "fin (ImpL <a>.M (x).N z) y"
   shows "z=y \<and> z\<sharp>M \<and> z\<sharp>[x].N"
 using a
 apply(erule_tac fin.cases)
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 apply(subgoal_tac "y\<sharp>[aa].Ma")
 apply(drule sym)
 apply(simp_all add: abs_fresh)
 apply (metis abs_fresh(5))
 done

                    fin_ImpL_elim fin_rest_elims
 
 lemma fin_rename:
   shows "fin M x \<Longrightarrow> fin ([(x',x)]\<bullet>M) x'"
 by (induct rule: fin.induct)
-   (auto simp add: calc_atm simp add: fresh_left abs_fresh)
+   (auto simp: calc_atm simp add: fresh_left abs_fresh)
 
 lemma not_fin_subst1:
   assumes a: "\<not>(fin M x)" 
   shows "\<not>(fin (M{c:=(y).P}) x)"
 using a [[simproc del: defined_all]]

 apply(simp add: fresh_fun_simp_AndR)
 apply(erule fin.cases, simp_all add: trm.inject)
 apply(rule exists_fresh'(2)[OF fs_coname1])
 apply(erule fin.cases, simp_all add: trm.inject)
 apply(drule fin_AndL1_elim)
-apply(auto simp add: abs_fresh)[1]
+apply(auto simp: abs_fresh)[1]
 apply(drule freshn_after_substc)
 apply(subgoal_tac "name2\<sharp>[name1]. trm")
 apply(simp add: fin.intros)
 apply(simp add: abs_fresh)
 apply(drule fin_AndL2_elim)
-apply(auto simp add: abs_fresh)[1]
+apply(auto simp: abs_fresh)[1]
 apply(drule freshn_after_substc)
 apply(subgoal_tac "name2\<sharp>[name1].trm")
 apply(simp add: fin.intros)
 apply(simp add: abs_fresh)
 apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(trm{coname2:=(y).P},coname1,P,x)")

 apply(simp add: fresh_fun_simp_OrR2)
 apply(erule fin.cases, simp_all add: trm.inject)
 apply(rule exists_fresh'(2)[OF fs_coname1])
 apply(erule fin.cases, simp_all add: trm.inject)
 apply(drule fin_OrL_elim)
-apply(auto simp add: abs_fresh)[1]
+apply(auto simp: abs_fresh)[1]
 apply(drule freshn_after_substc)+
 apply(subgoal_tac "name3\<sharp>[name1].trm1 \<and> name3\<sharp>[name2].trm2")
 apply(simp add: fin.intros)
 apply(simp add: abs_fresh)
 apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(trm{coname2:=(y).P},coname1,P,x)")

 apply(simp add: fresh_fun_simp_ImpR)
 apply(erule fin.cases, simp_all add: trm.inject)
 apply(rule exists_fresh'(2)[OF fs_coname1])
 apply(erule fin.cases, simp_all add: trm.inject)
 apply(drule fin_ImpL_elim)
-apply(auto simp add: abs_fresh)[1]
+apply(auto simp: abs_fresh)[1]
 apply(drule freshn_after_substc)+
 apply(subgoal_tac "x\<sharp>[name1].trm2")
 apply(simp add: fin.intros)
 apply(simp add: abs_fresh)
 done

 apply(erule conjE)+
 apply(simp add: fresh_fun_simp_AndL1)
 apply(erule fin.cases, simp_all add: trm.inject)
 apply(rule exists_fresh'(1)[OF fs_name1])
 apply(drule fin_AndL1_elim)
-apply(auto simp add: abs_fresh)[1]
+apply(auto simp: abs_fresh)[1]
 apply(drule freshn_after_substn)
 apply(simp)
 apply(subgoal_tac "name2\<sharp>[name1]. trm")
 apply(simp add: fin.intros)
 apply(simp add: abs_fresh)

 apply(erule conjE)+
 apply(simp add: fresh_fun_simp_AndL2)
 apply(erule fin.cases, simp_all add: trm.inject)
 apply(rule exists_fresh'(1)[OF fs_name1])
 apply(drule fin_AndL2_elim)
-apply(auto simp add: abs_fresh)[1]
+apply(auto simp: abs_fresh)[1]
 apply(drule freshn_after_substn)
 apply(simp)
 apply(subgoal_tac "name2\<sharp>[name1].trm")
 apply(simp add: fin.intros)
 apply(simp add: abs_fresh)

 apply(erule conjE)+
 apply(simp add: fresh_fun_simp_OrL)
 apply(erule fin.cases, simp_all add: trm.inject)
 apply(rule exists_fresh'(1)[OF fs_name1])
 apply(drule fin_OrL_elim)
-apply(auto simp add: abs_fresh)[1]
+apply(auto simp: abs_fresh)[1]
 apply(drule freshn_after_substn)
 apply(simp)
 apply(drule freshn_after_substn)
 apply(simp)
 apply(subgoal_tac "name3\<sharp>[name1].trm1 \<and> name3\<sharp>[name2].trm2")

 apply(erule conjE)+
 apply(simp add: fresh_fun_simp_ImpL)
 apply(erule fin.cases, simp_all add: trm.inject)
 apply(rule exists_fresh'(1)[OF fs_name1])
 apply(drule fin_ImpL_elim)
-apply(auto simp add: abs_fresh)[1]
+apply(auto simp: abs_fresh)[1]
 apply(drule freshn_after_substn)
 apply(simp)
 apply(drule freshn_after_substn)
 apply(simp)
 apply(subgoal_tac "x\<sharp>[name1].trm2")

 lemma fic_Ax_elim:
   assumes a: "fic (Ax x a) b"
   shows "a=b"
 using a
 apply(erule_tac fic.cases)
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 done
 
 lemma fic_NotR_elim:
   assumes a: "fic (NotR (x).M a) b"
   shows "a=b \<and> b\<sharp>M"
 using a
 apply(erule_tac fic.cases)
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 apply(subgoal_tac "b\<sharp>[xa].Ma")
 apply(drule sym)
 apply(simp_all add: abs_fresh)
 done
 
 lemma fic_OrR1_elim:
   assumes a: "fic (OrR1 <a>.M b) c"
   shows "b=c \<and> c\<sharp>[a].M"
 using a
 apply(erule_tac fic.cases)
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 done
 
 lemma fic_OrR2_elim:
   assumes a: "fic (OrR2 <a>.M b) c"
   shows "b=c \<and> c\<sharp>[a].M"
 using a
 apply(erule_tac fic.cases)
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 done
 
 lemma fic_AndR_elim:
   assumes a: "fic (AndR <a>.M <b>.N c) d"
   shows "c=d \<and> d\<sharp>[a].M \<and> d\<sharp>[b].N"
 using a
 apply(erule_tac fic.cases)
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 done
 
 lemma fic_ImpR_elim:
   assumes a: "fic (ImpR (x).<a>.M b) c"
   shows "b=c \<and> b\<sharp>[a].M"
 using a
 apply(erule_tac fic.cases)
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 apply(subgoal_tac "c\<sharp>[xa].[aa].Ma")
 apply(drule sym)
 apply(simp_all add: abs_fresh)
 done
 

                    fic_ImpR_elim fic_rest_elims
 
 lemma fic_rename:
   shows "fic M a \<Longrightarrow> fic ([(a',a)]\<bullet>M) a'"
 by (induct rule: fic.induct)
-   (auto simp add: calc_atm simp add: fresh_left abs_fresh)
+   (auto simp: calc_atm simp add: fresh_left abs_fresh)
 
 lemma not_fic_subst1:
   assumes a: "\<not>(fic M a)" 
   shows "\<not>(fic (M{y:=<c>.P}) a)"
 using a

   and   a::"coname"
   shows "M \<longrightarrow>\<^sub>l M' \<Longrightarrow> x\<sharp>M \<Longrightarrow> x\<sharp>M'"
   and   "M \<longrightarrow>\<^sub>l M' \<Longrightarrow> a\<sharp>M \<Longrightarrow> a\<sharp>M'"
 apply -
 apply(induct rule: l_redu.induct)
-apply(auto simp add: abs_fresh rename_fresh)
+apply(auto simp: abs_fresh rename_fresh)
 apply(case_tac "xa=x")
 apply(simp add: rename_fresh)
 apply(simp add: rename_fresh fresh_atm)
 apply(simp add: fresh_prod abs_fresh abs_supp fin_supp)+
 apply(induct rule: l_redu.induct)
-apply(auto simp add: abs_fresh rename_fresh)
+apply(auto simp: abs_fresh rename_fresh)
 apply(case_tac "aa=a")
 apply(simp add: rename_fresh)
 apply(simp add: rename_fresh fresh_atm)
 apply(simp add: fresh_prod abs_fresh abs_supp fin_supp)+
 done

 proof -
   assume fin: "fic M a"
   obtain x'::"name" where fs1: "x'\<sharp>(M,x)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(a,M,b)" by (rule exists_fresh(2), rule fin_supp, blast)
   have "Cut <a>.M (x).(Ax x b) =  Cut <a'>.([(a',a)]\<bullet>M) (x').(Ax x' b)"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>l ([(a',a)]\<bullet>M)[a'\<turnstile>c>b]" using fs1 fs2 fin
     by (auto intro: l_redu.intros simp add: fresh_left calc_atm fic_rename)
   also have "\<dots> = M[a\<turnstile>c>b]" using fs1 fs2 by (simp add: crename_rename)
   finally show ?thesis by simp
 qed

 proof -
   assume fin: "fin M x"
   obtain x'::"name" where fs1: "x'\<sharp>(y,M,x)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(a,M)" by (rule exists_fresh(2), rule fin_supp, blast)
   have "Cut <a>.(Ax y a) (x).M = Cut <a'>.(Ax y a') (x').([(x',x)]\<bullet>M)"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>l ([(x',x)]\<bullet>M)[x'\<turnstile>n>y]" using fs1 fs2 fin
     by (auto intro: l_redu.intros simp add: fresh_left calc_atm fin_rename)
   also have "\<dots> = M[x\<turnstile>n>y]" using fs1 fs2 by (simp add: nrename_rename)
   finally show ?thesis by simp
 qed

   obtain a'::"coname" where f3: "a'\<sharp>(a,M,N,b)" by (rule exists_fresh(2), rule fin_supp, blast)
   obtain b'::"coname" where f4: "b'\<sharp>(a,M,N,b,a')" by (rule exists_fresh(2), rule fin_supp, blast)
   have "Cut <a>.(NotR (x).M a) (y).(NotL <b>.N y) 
                       = Cut <a'>.(NotR (x).([(a',a)]\<bullet>M) a') (y').(NotL <b>.([(y',y)]\<bullet>N) y')"
     using f1 f2 f3 f4 
-    by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm abs_fresh)
+    by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm abs_fresh)
   also have "\<dots> = Cut <a'>.(NotR (x).M a') (y').(NotL <b>.N y')"
     using f1 f2 f3 f4 fs by (perm_simp)
   also have "\<dots> = Cut <a'>.(NotR (x').([(x',x)]\<bullet>M) a') (y').(NotL <b'>.([(b',b)]\<bullet>N) y')"
     using f1 f2 f3 f4 
-    by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>l Cut <b'>.([(b',b)]\<bullet>N) (x').([(x',x)]\<bullet>M)"
     using f1 f2 f3 f4 fs
     by (auto intro:  l_redu.intros simp add: fresh_prod fresh_left calc_atm fresh_atm)
   also have "\<dots> = Cut <b>.N (x).M"
-    using f1 f2 f3 f4 by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using f1 f2 f3 f4 by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   finally show ?thesis by simp
 qed 
 
 lemma better_LAnd1_intro[intro]:
   shows "\<lbrakk>a\<sharp>([b1].M1,[b2].M2); y\<sharp>[x].N\<rbrakk> 

   have "Cut <a>.(AndR <b1>.M1 <b2>.M2 a) (y).(AndL1 (x).N y)
                       = Cut <a'>.(AndR <b1>.M1 <b2>.M2 a') (y').(AndL1 (x).N y')"
     using f1 f2 f3 f4 fs
     apply(rule_tac sym)
     apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
-    apply(auto simp add: perm_fresh_fresh)
+    apply(auto simp: perm_fresh_fresh)
     done
   also have "\<dots> = Cut <a'>.(AndR <b1'>.([(b1',b1)]\<bullet>M1) <b2'>.([(b2',b2)]\<bullet>M2) a') 
                                                                (y').(AndL1 (x').([(x',x)]\<bullet>N) y')"
     using f1 f2 f3 f4 f5 fs 
     apply(rule_tac sym)

     done
   also have "\<dots> \<longrightarrow>\<^sub>l Cut <b1'>.([(b1',b1)]\<bullet>M1) (x').([(x',x)]\<bullet>N)"
     using f1 f2 f3 f4 f5 fs
     apply -
     apply(rule l_redu.intros)
-    apply(auto simp add: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
+    apply(auto simp: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
     done
   also have "\<dots> = Cut <b1>.M1 (x).N"
-    using f1 f2 f3 f4 f5 fs by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using f1 f2 f3 f4 f5 fs by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   finally show ?thesis by simp
 qed 
 
 lemma better_LAnd2_intro[intro]:
   shows "\<lbrakk>a\<sharp>([b1].M1,[b2].M2); y\<sharp>[x].N\<rbrakk> 

   have "Cut <a>.(AndR <b1>.M1 <b2>.M2 a) (y).(AndL2 (x).N y)
                       = Cut <a'>.(AndR <b1>.M1 <b2>.M2 a') (y').(AndL2 (x).N y')"
     using f1 f2 f3 f4 fs
     apply(rule_tac sym)
     apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
-    apply(auto simp add: perm_fresh_fresh)
+    apply(auto simp: perm_fresh_fresh)
     done
   also have "\<dots> = Cut <a'>.(AndR <b1'>.([(b1',b1)]\<bullet>M1) <b2'>.([(b2',b2)]\<bullet>M2) a') 
                                                                (y').(AndL2 (x').([(x',x)]\<bullet>N) y')"
     using f1 f2 f3 f4 f5 fs 
     apply(rule_tac sym)

     done
   also have "\<dots> \<longrightarrow>\<^sub>l Cut <b2'>.([(b2',b2)]\<bullet>M2) (x').([(x',x)]\<bullet>N)"
     using f1 f2 f3 f4 f5 fs
     apply -
     apply(rule l_redu.intros)
-    apply(auto simp add: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
+    apply(auto simp: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
     done
   also have "\<dots> = Cut <b2>.M2 (x).N"
-    using f1 f2 f3 f4 f5 fs by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using f1 f2 f3 f4 f5 fs by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   finally show ?thesis by simp
 qed
 
 lemma better_LOr1_intro[intro]:
   shows "\<lbrakk>y\<sharp>([x1].N1,[x2].N2); b\<sharp>[a].M\<rbrakk> 

   have "Cut <b>.(OrR1 <a>.M b) (y).(OrL (x1).N1 (x2).N2 y)
                       = Cut <b'>.(OrR1 <a>.M b') (y').(OrL (x1).N1 (x2).N2 y')"
     using f1 f2 f3 f4 f5 fs
     apply(rule_tac sym)
     apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
-    apply(auto simp add: perm_fresh_fresh)
+    apply(auto simp: perm_fresh_fresh)
     done
   also have "\<dots> = Cut <b'>.(OrR1 <a'>.([(a',a)]\<bullet>M) b') 
               (y').(OrL (x1').([(x1',x1)]\<bullet>N1) (x2').([(x2',x2)]\<bullet>N2) y')"   
     using f1 f2 f3 f4 f5 fs 
     apply(rule_tac sym)

     done
   also have "\<dots> \<longrightarrow>\<^sub>l Cut <a'>.([(a',a)]\<bullet>M) (x1').([(x1',x1)]\<bullet>N1)"
     using f1 f2 f3 f4 f5 fs
     apply -
     apply(rule l_redu.intros)
-    apply(auto simp add: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
+    apply(auto simp: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
     done
   also have "\<dots> = Cut <a>.M (x1).N1"
-    using f1 f2 f3 f4 f5 fs by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using f1 f2 f3 f4 f5 fs by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   finally show ?thesis by simp
 qed
 
 lemma better_LOr2_intro[intro]:
   shows "\<lbrakk>y\<sharp>([x1].N1,[x2].N2); b\<sharp>[a].M\<rbrakk> 

   have "Cut <b>.(OrR2 <a>.M b) (y).(OrL (x1).N1 (x2).N2 y)
                       = Cut <b'>.(OrR2 <a>.M b') (y').(OrL (x1).N1 (x2).N2 y')"
     using f1 f2 f3 f4 f5 fs
     apply(rule_tac sym)
     apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
-    apply(auto simp add: perm_fresh_fresh)
+    apply(auto simp: perm_fresh_fresh)
     done
   also have "\<dots> = Cut <b'>.(OrR2 <a'>.([(a',a)]\<bullet>M) b') 
               (y').(OrL (x1').([(x1',x1)]\<bullet>N1) (x2').([(x2',x2)]\<bullet>N2) y')"   
     using f1 f2 f3 f4 f5 fs 
     apply(rule_tac sym)

     done
   also have "\<dots> \<longrightarrow>\<^sub>l Cut <a'>.([(a',a)]\<bullet>M) (x2').([(x2',x2)]\<bullet>N2)"
     using f1 f2 f3 f4 f5 fs
     apply -
     apply(rule l_redu.intros)
-    apply(auto simp add: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
+    apply(auto simp: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
     done
   also have "\<dots> = Cut <a>.M (x2).N2"
-    using f1 f2 f3 f4 f5 fs by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using f1 f2 f3 f4 f5 fs by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   finally show ?thesis by simp
 qed 
 
 lemma better_LImp_intro[intro]:
   shows "\<lbrakk>z\<sharp>(N,[y].P); b\<sharp>[a].M; a\<sharp>N\<rbrakk> 

   have " Cut <b>.(ImpR (x).<a>.M b) (z).(ImpL <c>.N (y).P z)
                       =  Cut <b'>.(ImpR (x).<a>.M b') (z').(ImpL <c>.N (y).P z')"
     using f1 f2 f3 f4 f5 fs
     apply(rule_tac sym)
     apply(perm_simp add: trm.inject alpha calc_atm fresh_prod fresh_left fresh_atm abs_fresh)
-    apply(auto simp add: perm_fresh_fresh)
+    apply(auto simp: perm_fresh_fresh)
     done
   also have "\<dots> = Cut <b'>.(ImpR (x').<a'>.([(a',a)]\<bullet>([(x',x)]\<bullet>M)) b') 
                            (z').(ImpL <c'>.([(c',c)]\<bullet>N) (y').([(y',y)]\<bullet>P) z')"
     using f1 f2 f3 f4 f5 f6 fs 
     apply(rule_tac sym)

     done
   also have "\<dots> \<longrightarrow>\<^sub>l Cut <a'>.(Cut <c'>.([(c',c)]\<bullet>N) (x').([(a',a)]\<bullet>[(x',x)]\<bullet>M)) (y').([(y',y)]\<bullet>P)"
     using f1 f2 f3 f4 f5 f6 fs
     apply -
     apply(rule l_redu.intros)
-    apply(auto simp add: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
+    apply(auto simp: abs_fresh fresh_prod fresh_left calc_atm fresh_atm)
     done
   also have "\<dots> = Cut <a>.(Cut <c>.N (x).M) (y).P"
     using f1 f2 f3 f4 f5 f6 fs 
     apply(simp add: trm.inject)
     apply(rule conjI)

     apply(simp add: trm.inject)
     apply(rule conjI)
     apply(simp add: fresh_prod fresh_atm)
     apply(rule conjI)
     apply(perm_simp add: calc_atm)
-    apply(auto simp add: fresh_prod fresh_atm)[1]
+    apply(auto simp: fresh_prod fresh_atm)[1]
     apply(perm_simp add: alpha)
     apply(perm_simp add: alpha)
     apply(perm_simp add: alpha)
     apply(rule conjI)
     apply(perm_simp add: calc_atm)

   fixes M::"trm"
   and   a::"coname"
   assumes a: "[a].M = [b].N" "c\<sharp>(a,b,M,N)"
   shows "M = [(a,c)]\<bullet>[(b,c)]\<bullet>N"
 using a
-apply(auto simp add: alpha_fresh fresh_prod fresh_atm)
+apply(auto simp: alpha_fresh fresh_prod fresh_atm)
 apply(drule sym)
 apply(perm_simp)
 done 
 
 lemma alpha_name:
   fixes M::"trm"
   and   x::"name"
   assumes a: "[x].M = [y].N" "z\<sharp>(x,y,M,N)"
   shows "M = [(x,z)]\<bullet>[(y,z)]\<bullet>N"
 using a
-apply(auto simp add: alpha_fresh fresh_prod fresh_atm)
+apply(auto simp: alpha_fresh fresh_prod fresh_atm)
 apply(drule sym)
 apply(perm_simp)
 done 
 
 lemma alpha_name_coname:

   and   x::"name"
   and   a::"coname"
   assumes a: "[x].[b].M = [y].[c].N" "z\<sharp>(x,y,M,N)" "a\<sharp>(b,c,M,N)"
   shows "M = [(x,z)]\<bullet>[(b,a)]\<bullet>[(c,a)]\<bullet>[(y,z)]\<bullet>N"
 using a
-apply(auto simp add: alpha_fresh fresh_prod fresh_atm 
+apply(auto simp: alpha_fresh fresh_prod fresh_atm 
                      abs_supp fin_supp abs_fresh abs_perm fresh_left calc_atm)
 apply(drule sym)
 apply(simp)
 apply(perm_simp)
 done 

 apply(simp add: fresh_prod fresh_atm abs_fresh)
 apply(simp add: calc_atm)
 apply(rule exI)+
 apply(rule conjI)
 apply(rule refl)
-apply(auto simp add: calc_atm abs_fresh fresh_left)[1]
+apply(auto simp: calc_atm abs_fresh fresh_left)[1]
 apply(case_tac "y=x")
 apply(perm_simp)
 apply(perm_simp)
 apply(case_tac "aa=a")
 apply(perm_simp)

 apply(rule exI)+
 apply(rule conjI)
 apply(rule_tac s="x" and t="[(x,ca)]\<bullet>[(y,ca)]\<bullet>y" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh split: if_splits)[1]
 apply(generate_fresh "name")
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(auto)[1]
 apply(drule_tac z="cb" in  alpha_name)
 apply(simp add: fresh_prod fresh_atm abs_fresh)

 apply(rule exI)+
 apply(rule conjI)
 apply(rule_tac s="x" and t="[(x,cb)]\<bullet>[(y,cb)]\<bullet>y" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
 apply(perm_simp)+
 apply(generate_fresh "name")
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(auto)[1]
 apply(drule_tac z="cb" in  alpha_name)

 apply(rule exI)+
 apply(rule conjI)
 apply(rule_tac s="x" and t="[(x,cb)]\<bullet>[(y,cb)]\<bullet>y" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
 apply(perm_simp)+
 apply(generate_fresh "name")
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(auto)[1]
 apply(drule_tac z="cb" in  alpha_name)

 apply(rule exI)+
 apply(rule conjI)
 apply(rule_tac s="x" and t="[(x,cb)]\<bullet>[(y,cb)]\<bullet>y" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
 apply(perm_simp)+
 (* and2 case *)
 apply(rule disjI2)
 apply(rule disjI2)
 apply(rule disjI2)

 apply(rule exI)+
 apply(rule conjI)
 apply(rule_tac s="x" and t="[(x,ca)]\<bullet>[(y,ca)]\<bullet>y" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh split: if_splits)[1]
 apply(generate_fresh "name")
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(auto)[1]
 apply(drule_tac z="cb" in  alpha_name)
 apply(simp add: fresh_prod fresh_atm abs_fresh)

 apply(rule exI)+
 apply(rule conjI)
 apply(rule_tac s="x" and t="[(x,cb)]\<bullet>[(y,cb)]\<bullet>y" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
 apply(perm_simp)+
 apply(generate_fresh "name")
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(auto)[1]
 apply(drule_tac z="cb" in  alpha_name)

 apply(rule exI)+
 apply(rule conjI)
 apply(rule_tac s="x" and t="[(x,cb)]\<bullet>[(y,cb)]\<bullet>y" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
 apply(perm_simp)+
 apply(generate_fresh "name")
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(auto)[1]
 apply(drule_tac z="cb" in  alpha_name)

 apply(rule exI)+
 apply(rule conjI)
 apply(rule_tac s="x" and t="[(x,cb)]\<bullet>[(y,cb)]\<bullet>y" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
 apply(perm_simp)+
 (* or1 case *)
 apply(rule disjI2)
 apply(rule disjI2)
 apply(rule disjI2)

 apply(rule conjI)
 apply(rule exI)+
 apply(rule_tac s="x" and t="[(x,ca)]\<bullet>[(y,ca)]\<bullet>y" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
 apply(perm_simp)+
 apply(generate_fresh "name")
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(auto)[1]
 apply(drule_tac z="cb" in  alpha_name)

 apply(rule conjI)
 apply(rule exI)+
 apply(rule_tac s="x" and t="[(x,cb)]\<bullet>[(y,cb)]\<bullet>y" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
 apply(perm_simp)+
 (* or2 case *)
 apply(rule disjI2)
 apply(rule disjI2)
 apply(rule disjI2)

 apply(rule exI)+
 apply(rule conjI)
 apply(rule_tac s="x" and t="[(x,ca)]\<bullet>[(y,ca)]\<bullet>y" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
 apply(perm_simp)+
 apply(generate_fresh "name")
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(auto)[1]
 apply(drule_tac z="cb" in  alpha_name)

 apply(rule exI)+
 apply(rule conjI)
 apply(rule_tac s="x" and t="[(x,cb)]\<bullet>[(y,cb)]\<bullet>y" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
 apply(perm_simp)+
 (* imp-case *)
 apply(rule disjI2)
 apply(rule disjI2)
 apply(rule disjI2)

 apply(rule exI)+
 apply(rule conjI)
 apply(rule_tac s="x" and t="[(x,cb)]\<bullet>[(z,cb)]\<bullet>z" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
 apply(perm_simp)+
 apply(generate_fresh "name")
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(auto)[1]
 apply(drule_tac z="cc" in  alpha_name)

 apply(rule exI)+
 apply(rule conjI)
 apply(rule_tac s="x" and t="[(x,cc)]\<bullet>[(z,cc)]\<bullet>z" in subst)
 apply(simp add: calc_atm)
 apply(rule refl)
-apply(auto simp add: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
+apply(auto simp: fresh_left calc_atm abs_fresh alpha perm_fresh_fresh split: if_splits)[1]
 apply(perm_simp)+
 done
 
 inductive
   c_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^sub>c _" [100,100] 100)

 proof -
   assume not_fic: "\<not>fic M a"
   obtain x'::"name" where fs1: "x'\<sharp>(N,M,x)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(a,M,N)" by (rule exists_fresh(2), rule fin_supp, blast)
   have "Cut <a>.M (x).N =  Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N)"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>c ([(a',a)]\<bullet>M){a':=(x').([(x',x)]\<bullet>N)}" using fs1 fs2 not_fic
     apply -
     apply(rule left)
     apply(clarify)
     apply(drule_tac a'="a" in fic_rename)

 proof -
   assume not_fin: "\<not>fin N x"
   obtain x'::"name" where fs1: "x'\<sharp>(N,M,x)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(a,M,N)" by (rule exists_fresh(2), rule fin_supp, blast)
   have "Cut <a>.M (x).N =  Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N)"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>c ([(x',x)]\<bullet>N){x':=<a'>.([(a',a)]\<bullet>M)}" using fs1 fs2 not_fin
     apply -
     apply(rule right)
     apply(clarify)
     apply(drule_tac x'="x" in fin_rename)

   and   c::"coname"
   shows "M \<longrightarrow>\<^sub>c M' \<Longrightarrow> x\<sharp>M \<Longrightarrow> x\<sharp>M'"
   and   "M \<longrightarrow>\<^sub>c M' \<Longrightarrow> c\<sharp>M \<Longrightarrow> c\<sharp>M'"
 apply -
 apply(induct rule: c_redu.induct)
-apply(auto simp add: abs_fresh rename_fresh subst_fresh)
+apply(auto simp: abs_fresh rename_fresh subst_fresh)
 apply(induct rule: c_redu.induct)
-apply(auto simp add: abs_fresh rename_fresh subst_fresh)
+apply(auto simp: abs_fresh rename_fresh subst_fresh)
 done
 
 inductive
   a_redu :: "trm \<Rightarrow> trm \<Rightarrow> bool" ("_ \<longrightarrow>\<^sub>a _" [100,100] 100)
 where

   and   "M \<longrightarrow>\<^sub>a M' \<Longrightarrow> c\<sharp>M \<Longrightarrow> c\<sharp>M'"
 apply -
 apply(induct rule: a_redu.induct)
 apply(simp add: fresh_l_redu)
 apply(simp add: fresh_c_redu)
-apply(auto simp add: abs_fresh abs_supp fin_supp)
+apply(auto simp: abs_fresh abs_supp fin_supp)
 apply(induct rule: a_redu.induct)
 apply(simp add: fresh_l_redu)
 apply(simp add: fresh_c_redu)
-apply(auto simp add: abs_fresh abs_supp fin_supp)
+apply(auto simp: abs_fresh abs_supp fin_supp)
 done
 
 equivariance a_redu
 
 nominal_inductive a_redu

 proof -
   assume red: "M\<longrightarrow>\<^sub>a M'"
   obtain x'::"name"   where fs1: "x'\<sharp>(M,N,x)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a)" by (rule exists_fresh(2), rule fin_supp, blast)
   have "Cut <a>.M (x).N =  Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N)"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a  Cut <a'>.([(a',a)]\<bullet>M') (x').([(x',x)]\<bullet>N)" using fs1 fs2 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt)
   also have "\<dots> = Cut <a>.M' (x).N" 
-    using fs1 fs2 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
 lemma better_CutR_intro[intro]:
   shows "N\<longrightarrow>\<^sub>a N' \<Longrightarrow> Cut <a>.M (x).N \<longrightarrow>\<^sub>a Cut <a>.M (x).N'"
 proof -
   assume red: "N\<longrightarrow>\<^sub>a N'"
   obtain x'::"name"   where fs1: "x'\<sharp>(M,N,x)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a)" by (rule exists_fresh(2), rule fin_supp, blast)
   have "Cut <a>.M (x).N =  Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N)"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a  Cut <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N')" using fs1 fs2 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt)
   also have "\<dots> = Cut <a>.M (x).N'" 
-    using fs1 fs2 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
     
 lemma better_AndRL_intro[intro]:
   shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> AndR <a>.M <b>.N c \<longrightarrow>\<^sub>a AndR <a>.M' <b>.N c"
 proof -
   assume red: "M\<longrightarrow>\<^sub>a M'"
   obtain b'::"coname" where fs1: "b'\<sharp>(M,N,a,b,c)" by (rule exists_fresh(2), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a,b,c,b')" by (rule exists_fresh(2), rule fin_supp, blast)
   have "AndR <a>.M <b>.N c =  AndR <a'>.([(a',a)]\<bullet>M) <b'>.([(b',b)]\<bullet>N) c"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a  AndR <a'>.([(a',a)]\<bullet>M') <b'>.([(b',b)]\<bullet>N) c" using fs1 fs2 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
   also have "\<dots> = AndR <a>.M' <b>.N c" 
-    using fs1 fs2 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
 lemma better_AndRR_intro[intro]:
   shows "N\<longrightarrow>\<^sub>a N' \<Longrightarrow> AndR <a>.M <b>.N c \<longrightarrow>\<^sub>a AndR <a>.M <b>.N' c"
 proof -
   assume red: "N\<longrightarrow>\<^sub>a N'"
   obtain b'::"coname" where fs1: "b'\<sharp>(M,N,a,b,c)" by (rule exists_fresh(2), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a,b,c,b')" by (rule exists_fresh(2), rule fin_supp, blast)
   have "AndR <a>.M <b>.N c =  AndR <a'>.([(a',a)]\<bullet>M) <b'>.([(b',b)]\<bullet>N) c"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a  AndR <a'>.([(a',a)]\<bullet>M) <b'>.([(b',b)]\<bullet>N') c" using fs1 fs2 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
   also have "\<dots> = AndR <a>.M <b>.N' c" 
-    using fs1 fs2 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
 lemma better_AndL1_intro[intro]:
   shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> AndL1 (x).M y \<longrightarrow>\<^sub>a AndL1 (x).M' y"
 proof -
   assume red: "M\<longrightarrow>\<^sub>a M'"
   obtain x'::"name" where fs1: "x'\<sharp>(M,y,x)" by (rule exists_fresh(1), rule fin_supp, blast)
   have "AndL1 (x).M y = AndL1 (x').([(x',x)]\<bullet>M) y"
-    using fs1 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a AndL1 (x').([(x',x)]\<bullet>M') y" using fs1 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
   also have "\<dots> = AndL1 (x).M' y" 
-    using fs1 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
 lemma better_AndL2_intro[intro]:
   shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> AndL2 (x).M y \<longrightarrow>\<^sub>a AndL2 (x).M' y"
 proof -
   assume red: "M\<longrightarrow>\<^sub>a M'"
   obtain x'::"name" where fs1: "x'\<sharp>(M,y,x)" by (rule exists_fresh(1), rule fin_supp, blast)
   have "AndL2 (x).M y = AndL2 (x').([(x',x)]\<bullet>M) y"
-    using fs1 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a AndL2 (x').([(x',x)]\<bullet>M') y" using fs1 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
   also have "\<dots> = AndL2 (x).M' y" 
-    using fs1 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
 lemma better_OrLL_intro[intro]:
   shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> OrL (x).M (y).N z \<longrightarrow>\<^sub>a OrL (x).M' (y).N z"
 proof -
   assume red: "M\<longrightarrow>\<^sub>a M'"
   obtain x'::"name" where fs1: "x'\<sharp>(M,N,x,y,z)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain y'::"name" where fs2: "y'\<sharp>(M,N,x,y,z,x')" by (rule exists_fresh(1), rule fin_supp, blast)
   have "OrL (x).M (y).N z =  OrL (x').([(x',x)]\<bullet>M) (y').([(y',y)]\<bullet>N) z"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a OrL (x').([(x',x)]\<bullet>M') (y').([(y',y)]\<bullet>N) z" using fs1 fs2 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
   also have "\<dots> = OrL (x).M' (y).N z" 
-    using fs1 fs2 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
 lemma better_OrLR_intro[intro]:
   shows "N\<longrightarrow>\<^sub>a N' \<Longrightarrow> OrL (x).M (y).N z \<longrightarrow>\<^sub>a OrL (x).M (y).N' z"
 proof -
   assume red: "N\<longrightarrow>\<^sub>a N'"
   obtain x'::"name" where fs1: "x'\<sharp>(M,N,x,y,z)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain y'::"name" where fs2: "y'\<sharp>(M,N,x,y,z,x')" by (rule exists_fresh(1), rule fin_supp, blast)
   have "OrL (x).M (y).N z =  OrL (x').([(x',x)]\<bullet>M) (y').([(y',y)]\<bullet>N) z"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a OrL (x').([(x',x)]\<bullet>M) (y').([(y',y)]\<bullet>N') z" using fs1 fs2 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
   also have "\<dots> = OrL (x).M (y).N' z" 
-    using fs1 fs2 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
 lemma better_OrR1_intro[intro]:
   shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> OrR1 <a>.M b \<longrightarrow>\<^sub>a OrR1 <a>.M' b"
 proof -
   assume red: "M\<longrightarrow>\<^sub>a M'"
   obtain a'::"coname" where fs1: "a'\<sharp>(M,b,a)" by (rule exists_fresh(2), rule fin_supp, blast)
   have "OrR1 <a>.M b = OrR1 <a'>.([(a',a)]\<bullet>M) b"
-    using fs1 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a OrR1 <a'>.([(a',a)]\<bullet>M') b" using fs1 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
   also have "\<dots> = OrR1 <a>.M' b" 
-    using fs1 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
 lemma better_OrR2_intro[intro]:
   shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> OrR2 <a>.M b \<longrightarrow>\<^sub>a OrR2 <a>.M' b"
 proof -
   assume red: "M\<longrightarrow>\<^sub>a M'"
   obtain a'::"coname" where fs1: "a'\<sharp>(M,b,a)" by (rule exists_fresh(2), rule fin_supp, blast)
   have "OrR2 <a>.M b = OrR2 <a'>.([(a',a)]\<bullet>M) b"
-    using fs1 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a OrR2 <a'>.([(a',a)]\<bullet>M') b" using fs1 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
   also have "\<dots> = OrR2 <a>.M' b" 
-    using fs1 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs1 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
 lemma better_ImpLL_intro[intro]:
   shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> ImpL <a>.M (x).N y \<longrightarrow>\<^sub>a ImpL <a>.M' (x).N y"
 proof -
   assume red: "M\<longrightarrow>\<^sub>a M'"
   obtain x'::"name"   where fs1: "x'\<sharp>(M,N,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a)" by (rule exists_fresh(2), rule fin_supp, blast)
   have "ImpL <a>.M (x).N y =  ImpL <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N) y"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a  ImpL <a'>.([(a',a)]\<bullet>M') (x').([(x',x)]\<bullet>N) y" using fs1 fs2 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
   also have "\<dots> = ImpL <a>.M' (x).N y" 
-    using fs1 fs2 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
 lemma better_ImpLR_intro[intro]:
   shows "N\<longrightarrow>\<^sub>a N' \<Longrightarrow> ImpL <a>.M (x).N y \<longrightarrow>\<^sub>a ImpL <a>.M (x).N' y"
 proof -
   assume red: "N\<longrightarrow>\<^sub>a N'"
   obtain x'::"name"   where fs1: "x'\<sharp>(M,N,x,y)" by (rule exists_fresh(1), rule fin_supp, blast)
   obtain a'::"coname" where fs2: "a'\<sharp>(M,N,a)" by (rule exists_fresh(2), rule fin_supp, blast)
   have "ImpL <a>.M (x).N y =  ImpL <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N) y"
-    using fs1 fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs1 fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a  ImpL <a'>.([(a',a)]\<bullet>M) (x').([(x',x)]\<bullet>N') y" using fs1 fs2 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
   also have "\<dots> = ImpL <a>.M (x).N' y" 
-    using fs1 fs2 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs1 fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
 lemma better_ImpR_intro[intro]:
   shows "M\<longrightarrow>\<^sub>a M' \<Longrightarrow> ImpR (x).<a>.M b \<longrightarrow>\<^sub>a ImpR (x).<a>.M' b"
 proof -
   assume red: "M\<longrightarrow>\<^sub>a M'"
   obtain a'::"coname" where fs2: "a'\<sharp>(M,a,b)" by (rule exists_fresh(2), rule fin_supp, blast)
   have "ImpR (x).<a>.M b = ImpR (x).<a'>.([(a',a)]\<bullet>M) b"
-    using fs2 by (rule_tac sym, auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm)
+    using fs2 by (rule_tac sym, auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm)
   also have "\<dots> \<longrightarrow>\<^sub>a ImpR (x).<a'>.([(a',a)]\<bullet>M') b" using fs2 red
     by (auto intro: a_redu.intros simp add: fresh_left calc_atm a_redu.eqvt fresh_atm fresh_prod)
   also have "\<dots> = ImpR (x).<a>.M' b" 
-    using fs2 red by (auto simp add: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
+    using fs2 red by (auto simp: trm.inject alpha fresh_atm fresh_prod calc_atm fresh_a_redu)
   finally show ?thesis by simp
 qed
 
 text \<open>axioms do not reduce\<close>
 

 by (erule_tac c_redu.cases) (simp_all add: trm.inject)
 
 lemma ax_do_not_a_reduce:
   shows "Ax x a \<longrightarrow>\<^sub>a M \<Longrightarrow> False"
 apply(erule_tac a_redu.cases) 
-apply(auto simp add: trm.inject)
+apply(auto simp: trm.inject)
 apply(drule ax_do_not_l_reduce)
 apply(simp)
 apply(drule ax_do_not_c_reduce)
 apply(simp)
 done

 apply(auto)
 apply(rotate_tac 2)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
-apply(auto simp add: alpha a_redu.eqvt)
+apply(auto simp: alpha a_redu.eqvt)
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
 apply(simp add: perm_swap)
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
 apply(simp add: perm_swap)
 done
 
 lemma a_redu_NotR_elim:
   assumes a: "NotR (x).M a \<longrightarrow>\<^sub>a R"

 apply(auto)
 apply(rotate_tac 2)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
-apply(auto simp add: alpha a_redu.eqvt)
+apply(auto simp: alpha a_redu.eqvt)
 apply(rule_tac x="([(x,xa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
 apply(simp add: perm_swap)
 apply(rule_tac x="([(x,xaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
 apply(simp add: perm_swap)
 done
 
 lemma a_redu_AndR_elim:
   assumes a: "AndR <a>.M <b>.N c\<longrightarrow>\<^sub>a R"

 apply(rotate_tac 6)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
 apply(rule disjI1)
-apply(auto simp add: alpha a_redu.eqvt)[1]
+apply(auto simp: alpha a_redu.eqvt)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI) 
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule disjI2)
-apply(auto simp add: alpha a_redu.eqvt)[1]
+apply(auto simp: alpha a_redu.eqvt)[1]
 apply(rule_tac x="([(b,ba)]\<bullet>N')" in exI) 
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,baa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,ba)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,baa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,ba)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,baa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,ba)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,baa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rotate_tac 6)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
 apply(rule disjI1)
-apply(auto simp add: alpha a_redu.eqvt)[1]
+apply(auto simp: alpha a_redu.eqvt)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M')" in exI) 
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule disjI2)
-apply(auto simp add: alpha a_redu.eqvt)[1]
+apply(auto simp: alpha a_redu.eqvt)[1]
 apply(rule_tac x="([(b,ba)]\<bullet>N'a)" in exI) 
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,ba)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,ba)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,ba)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,baa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,baa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,baa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(b,baa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 done
 
 lemma a_redu_AndL1_elim:
   assumes a: "AndL1 (x).M y \<longrightarrow>\<^sub>a R"
   shows "\<exists>M'. R = AndL1 (x).M' y \<and> M\<longrightarrow>\<^sub>aM'"

 apply(auto)
 apply(rotate_tac 3)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
-apply(auto simp add: alpha a_redu.eqvt)
+apply(auto simp: alpha a_redu.eqvt)
 apply(rule_tac x="([(x,xa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
 apply(simp add: perm_swap)
 apply(rule_tac x="([(x,xaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
 apply(simp add: perm_swap)
 done
 
 lemma a_redu_AndL2_elim:
   assumes a: "AndL2 (x).M y \<longrightarrow>\<^sub>a R"

 apply(auto)
 apply(rotate_tac 3)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
-apply(auto simp add: alpha a_redu.eqvt)
+apply(auto simp: alpha a_redu.eqvt)
 apply(rule_tac x="([(x,xa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
 apply(simp add: perm_swap)
 apply(rule_tac x="([(x,xaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
 apply(simp add: perm_swap)
 done
 
 lemma a_redu_OrL_elim:
   assumes a: "OrL (x).M (y).N z\<longrightarrow>\<^sub>a R"

 apply(rotate_tac 6)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
 apply(rule disjI1)
-apply(auto simp add: alpha a_redu.eqvt)[1]
+apply(auto simp: alpha a_redu.eqvt)[1]
 apply(rule_tac x="([(x,xa)]\<bullet>M'a)" in exI) 
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule disjI2)
-apply(auto simp add: alpha a_redu.eqvt)[1]
+apply(auto simp: alpha a_redu.eqvt)[1]
 apply(rule_tac x="([(y,ya)]\<bullet>N')" in exI) 
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,yaa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,ya)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,yaa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,ya)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,yaa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,ya)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,yaa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rotate_tac 6)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
 apply(rule disjI1)
-apply(auto simp add: alpha a_redu.eqvt)[1]
+apply(auto simp: alpha a_redu.eqvt)[1]
 apply(rule_tac x="([(x,xa)]\<bullet>M')" in exI) 
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xaa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xaa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xaa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(x,xaa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule disjI2)
-apply(auto simp add: alpha a_redu.eqvt)[1]
+apply(auto simp: alpha a_redu.eqvt)[1]
 apply(rule_tac x="([(y,ya)]\<bullet>N'a)" in exI) 
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,ya)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,ya)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,ya)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,yaa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,yaa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,yaa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,yaa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 done
 
 lemma a_redu_OrR1_elim:
   assumes a: "OrR1 <a>.M b \<longrightarrow>\<^sub>a R"
   shows "\<exists>M'. R = OrR1 <a>.M' b \<and> M\<longrightarrow>\<^sub>aM'"

 apply(auto)
 apply(rotate_tac 3)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
-apply(auto simp add: alpha a_redu.eqvt)
+apply(auto simp: alpha a_redu.eqvt)
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
 apply(simp add: perm_swap)
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
 apply(simp add: perm_swap)
 done
 
 lemma a_redu_OrR2_elim:
   assumes a: "OrR2 <a>.M b \<longrightarrow>\<^sub>a R"

 apply(auto)
 apply(rotate_tac 3)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
-apply(auto simp add: alpha a_redu.eqvt)
+apply(auto simp: alpha a_redu.eqvt)
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
 apply(simp add: perm_swap)
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)
 apply(simp add: perm_swap)
 done
 
 lemma a_redu_ImpL_elim:
   assumes a: "ImpL <a>.M (y).N z\<longrightarrow>\<^sub>a R"

 apply(rotate_tac 5)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
 apply(rule disjI1)
-apply(auto simp add: alpha a_redu.eqvt)[1]
+apply(auto simp: alpha a_redu.eqvt)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI) 
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule disjI2)
-apply(auto simp add: alpha a_redu.eqvt)[1]
+apply(auto simp: alpha a_redu.eqvt)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N')" in exI) 
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rotate_tac 5)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
 apply(rule disjI1)
-apply(auto simp add: alpha a_redu.eqvt)[1]
+apply(auto simp: alpha a_redu.eqvt)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M')" in exI) 
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(a,aaa)]\<bullet>M')" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule disjI2)
-apply(auto simp add: alpha a_redu.eqvt)[1]
+apply(auto simp: alpha a_redu.eqvt)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N'a)" in exI) 
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 apply(rule_tac x="([(y,xa)]\<bullet>N'a)" in exI)
-apply(auto simp add: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
+apply(auto simp: perm_swap fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu)[1]
 done
 
 lemma a_redu_ImpR_elim:
   assumes a: "ImpR (x).<a>.M b \<longrightarrow>\<^sub>a R"
   shows "\<exists>M'. R = ImpR (x).<a>.M' b \<and> M\<longrightarrow>\<^sub>aM'"

 apply(auto)
 apply(rotate_tac 3)
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
-apply(auto simp add: alpha a_redu.eqvt abs_perm abs_fresh)
+apply(auto simp: alpha a_redu.eqvt abs_perm abs_fresh)
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
 apply(rule_tac x="([(a,aa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
 apply(rule_tac x="([(a,aaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
 apply(rule_tac x="([(x,xa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
 apply(rule_tac x="([(x,xa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
 apply(rule_tac x="([(a,aa)]\<bullet>[(x,xa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
 apply(rule sym)
 apply(rule trans)
 apply(rule perm_compose)
 apply(simp add: calc_atm perm_swap)
 apply(rule_tac x="([(a,aaa)]\<bullet>[(x,xa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
 apply(rule sym)
 apply(rule trans)
 apply(rule perm_compose)
 apply(simp add: calc_atm perm_swap)
 apply(rule_tac x="([(x,xaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
 apply(rule_tac x="([(x,xaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
 apply(rule_tac x="([(a,aa)]\<bullet>[(x,xaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
 apply(rule sym)
 apply(rule trans)
 apply(rule perm_compose)
 apply(simp add: calc_atm perm_swap)
 apply(rule_tac x="([(a,aaa)]\<bullet>[(x,xaa)]\<bullet>M'a)" in exI)
-apply(auto simp add: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
+apply(auto simp: fresh_left alpha a_redu.eqvt calc_atm fresh_a_redu perm_swap)
 apply(rule sym)
 apply(rule trans)
 apply(rule perm_compose)
 apply(simp add: calc_atm perm_swap)
 done

   shows "(\<exists>M' N'. R = AndR <a>.M' <b>.N' c \<and> M \<longrightarrow>\<^sub>a* M' \<and> N \<longrightarrow>\<^sub>a* N')"
 using a
 apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_AndR_elim)
-apply(auto simp add: alpha trm.inject)
+apply(auto simp: alpha trm.inject)
 done
 
 lemma a_star_redu_AndL1_elim:
   assumes a: "AndL1 (x).M y \<longrightarrow>\<^sub>a* R"
   shows "\<exists>M'. R = AndL1 (x).M' y \<and> M \<longrightarrow>\<^sub>a* M'"
 using a
 apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_AndL1_elim)
-apply(auto simp add: alpha trm.inject)
+apply(auto simp: alpha trm.inject)
 done
 
 lemma a_star_redu_AndL2_elim:
   assumes a: "AndL2 (x).M y \<longrightarrow>\<^sub>a* R"
   shows "\<exists>M'. R = AndL2 (x).M' y \<and> M \<longrightarrow>\<^sub>a* M'"
 using a
 apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_AndL2_elim)
-apply(auto simp add: alpha trm.inject)
+apply(auto simp: alpha trm.inject)
 done
 
 lemma a_star_redu_OrL_elim:
   assumes a: "OrL (x).M (y).N z \<longrightarrow>\<^sub>a* R"
   shows "(\<exists>M' N'. R = OrL (x).M' (y).N' z \<and> M \<longrightarrow>\<^sub>a* M' \<and> N \<longrightarrow>\<^sub>a* N')"
 using a
 apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_OrL_elim)
-apply(auto simp add: alpha trm.inject)
+apply(auto simp: alpha trm.inject)
 done
 
 lemma a_star_redu_OrR1_elim:
   assumes a: "OrR1 <a>.M y \<longrightarrow>\<^sub>a* R"
   shows "\<exists>M'. R = OrR1 <a>.M' y \<and> M \<longrightarrow>\<^sub>a* M'"
 using a
 apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_OrR1_elim)
-apply(auto simp add: alpha trm.inject)
+apply(auto simp: alpha trm.inject)
 done
 
 lemma a_star_redu_OrR2_elim:
   assumes a: "OrR2 <a>.M y \<longrightarrow>\<^sub>a* R"
   shows "\<exists>M'. R = OrR2 <a>.M' y \<and> M \<longrightarrow>\<^sub>a* M'"
 using a
 apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_OrR2_elim)
-apply(auto simp add: alpha trm.inject)
+apply(auto simp: alpha trm.inject)
 done
 
 lemma a_star_redu_ImpR_elim:
   assumes a: "ImpR (x).<a>.M y \<longrightarrow>\<^sub>a* R"
   shows "\<exists>M'. R = ImpR (x).<a>.M' y \<and> M \<longrightarrow>\<^sub>a* M'"
 using a
 apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_ImpR_elim)
-apply(auto simp add: alpha trm.inject)
+apply(auto simp: alpha trm.inject)
 done
 
 lemma a_star_redu_ImpL_elim:
   assumes a: "ImpL <a>.M (y).N z \<longrightarrow>\<^sub>a* R"
   shows "(\<exists>M' N'. R = ImpL <a>.M' (y).N' z \<and> M \<longrightarrow>\<^sub>a* M' \<and> N \<longrightarrow>\<^sub>a* N')"
 using a
 apply(induct set: rtranclp)
 apply(auto)
 apply(drule a_redu_ImpL_elim)
-apply(auto simp add: alpha trm.inject)
+apply(auto simp: alpha trm.inject)
 done
 
 text \<open>Substitution\<close>
 
 lemma subst_not_fin1:

   assumes  a: "fin M x"
   and      b: "M \<longrightarrow>\<^sub>a* M'"
   shows "fin M' x"
 using b a
 apply(induct set: rtranclp)
-apply(auto simp add: fin_a_reduce)
+apply(auto simp: fin_a_reduce)
 done
 
 lemma fic_l_reduce:
   assumes  a: "fic M x"
   and      b: "M \<longrightarrow>\<^sub>l M'"

   assumes  a: "fic M x"
   and      b: "M \<longrightarrow>\<^sub>a* M'"
   shows "fic M' x"
 using b a
 apply(induct set: rtranclp)
-apply(auto simp add: fic_a_reduce)
+apply(auto simp: fic_a_reduce)
 done
 
 text \<open>substitution properties\<close>
 
 lemma subst_with_ax1:

       apply(rule better_LAxL_intro)
       apply(rule fin.intros)
       apply(simp add: abs_fresh)
       done
     also have "\<dots> = AndL1 (u).(M{x:=<a>.Ax y a}) y" using fs new
-      by (auto simp add: fresh_prod fresh_atm nrename_fresh)
+      by (auto simp: fresh_prod fresh_atm nrename_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* AndL1 (u).(M[x\<turnstile>n>y]) y" using ih by (auto intro: a_star_congs)
     also have "\<dots> = (AndL1 (u).M v)[x\<turnstile>n>y]" using eq fs by simp
     finally show "(AndL1 (u).M v){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (AndL1 (u).M v)[x\<turnstile>n>y]" by simp
   next
     case False

       apply(rule better_LAxL_intro)
       apply(rule fin.intros)
       apply(simp add: abs_fresh)
       done
     also have "\<dots> = AndL2 (u).(M{x:=<a>.Ax y a}) y" using fs new
-      by (auto simp add: fresh_prod fresh_atm nrename_fresh)
+      by (auto simp: fresh_prod fresh_atm nrename_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* AndL2 (u).(M[x\<turnstile>n>y]) y" using ih by (auto intro: a_star_congs)
     also have "\<dots> = (AndL2 (u).M v)[x\<turnstile>n>y]" using eq fs by simp
     finally show "(AndL2 (u).M v){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (AndL2 (u).M v)[x\<turnstile>n>y]" by simp
   next
     case False

       apply(rule better_LAxL_intro)
       apply(rule fin.intros)
       apply(simp_all add: abs_fresh)
       done
     also have "\<dots> = OrL (u).(M{x:=<a>.Ax y a}) (v).(N{x:=<a>.Ax y a}) y" using fs new
-      by (auto simp add: fresh_prod fresh_atm nrename_fresh subst_fresh)
+      by (auto simp: fresh_prod fresh_atm nrename_fresh subst_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* OrL (u).(M[x\<turnstile>n>y]) (v).(N[x\<turnstile>n>y]) y" 
       using ih1 ih2 by (auto intro: a_star_congs)
     also have "\<dots> = (OrL (u).M (v).N z)[x\<turnstile>n>y]" using eq fs by simp
     finally show "(OrL (u).M (v).N z){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (OrL (u).M (v).N z)[x\<turnstile>n>y]" by simp
   next

       apply(rule better_LAxL_intro)
       apply(rule fin.intros)
       apply(simp_all add: abs_fresh)
       done
     also have "\<dots> = ImpL <c>.(M{x:=<a>.Ax y a}) (u).(N{x:=<a>.Ax y a}) y" using fs new
-      by (auto simp add: fresh_prod subst_fresh fresh_atm trm.inject alpha rename_fresh)
+      by (auto simp: fresh_prod subst_fresh fresh_atm trm.inject alpha rename_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* ImpL <c>.(M[x\<turnstile>n>y]) (u).(N[x\<turnstile>n>y]) y" 
       using ih1 ih2 by (auto intro: a_star_congs)
     also have "\<dots> = (ImpL <c>.M (u).N v)[x\<turnstile>n>y]" using eq fs by simp
     finally show "(ImpL <c>.M (u).N v){x:=<a>.Ax y a} \<longrightarrow>\<^sub>a* (ImpL <c>.M (u).N v)[x\<turnstile>n>y]" using fs by simp
   next

       apply(rule better_LAxR_intro)
       apply(rule fic.intros)
       apply(simp_all add: abs_fresh)
       done
     also have "\<dots> = AndR <c>.(M{b:=(x).Ax x a}) <d>.(N{b:=(x).Ax x a}) a" using fs new
-      by (auto simp add: fresh_prod fresh_atm subst_fresh crename_fresh)
+      by (auto simp: fresh_prod fresh_atm subst_fresh crename_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* AndR <c>.(M[b\<turnstile>c>a]) <d>.(N[b\<turnstile>c>a]) a" using ih1 ih2 by (auto intro: a_star_congs)
     also have "\<dots> = (AndR <c>.M <d>.N e)[b\<turnstile>c>a]" using eq fs by simp
     finally show "(AndR <c>.M <d>.N e){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (AndR <c>.M <d>.N e)[b\<turnstile>c>a]" by simp
   next
     case False

       apply(rule better_LAxR_intro)
       apply(rule fic.intros)
       apply(simp_all add: abs_fresh)
       done
     also have "\<dots> = OrR1 <c>.M{b:=(x).Ax x a} a" using fs new
-      by (auto simp add: fresh_prod fresh_atm crename_fresh subst_fresh)
+      by (auto simp: fresh_prod fresh_atm crename_fresh subst_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* OrR1 <c>.(M[b\<turnstile>c>a]) a" using ih by (auto intro: a_star_congs)
     also have "\<dots> = (OrR1 <c>.M d)[b\<turnstile>c>a]" using eq fs by simp
     finally show "(OrR1 <c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (OrR1 <c>.M d)[b\<turnstile>c>a]" by simp
   next
     case False

       apply(rule better_LAxR_intro)
       apply(rule fic.intros)
       apply(simp_all add: abs_fresh)
       done
     also have "\<dots> = OrR2 <c>.M{b:=(x).Ax x a} a" using fs new
-      by (auto simp add: fresh_prod fresh_atm crename_fresh subst_fresh)
+      by (auto simp: fresh_prod fresh_atm crename_fresh subst_fresh)
     also have "\<dots> \<longrightarrow>\<^sub>a* OrR2 <c>.(M[b\<turnstile>c>a]) a" using ih by (auto intro: a_star_congs)
     also have "\<dots> = (OrR2 <c>.M d)[b\<turnstile>c>a]" using eq fs by simp
     finally show "(OrR2 <c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (OrR2 <c>.M d)[b\<turnstile>c>a]" by simp
   next
     case False

       apply(rule better_LAxR_intro)
       apply(rule fic.intros)
       apply(simp_all add: abs_fresh)
       done
     also have "\<dots> = ImpR z.<c>.M{b:=(x).Ax x a} a" using fs new
-      by (auto simp add: fresh_prod crename_fresh subst_fresh fresh_atm)
+      by (auto simp: fresh_prod crename_fresh subst_fresh fresh_atm)
     also have "\<dots> \<longrightarrow>\<^sub>a* ImpR z.<c>.(M[b\<turnstile>c>a]) a" using ih by (auto intro: a_star_congs)
     also have "\<dots> = (ImpR z.<c>.M b)[b\<turnstile>c>a]" using eq fs by simp
     finally show "(ImpR (z).<c>.M d){b:=(x).Ax x a} \<longrightarrow>\<^sub>a* (ImpR (z).<c>.M d)[b\<turnstile>c>a]" using eq by simp
   next
     case False

 text \<open>substitution lemmas\<close>
 
 lemma not_Ax1:
   shows "\<not>(b\<sharp>M) \<Longrightarrow> M{b:=(y).Q} \<noteq> Ax x a"
 apply(nominal_induct M avoiding: b y Q x a rule: trm.strong_induct)
-apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
+apply(auto simp: fresh_atm abs_fresh abs_supp fin_supp)
 apply(subgoal_tac "\<exists>x'::coname. x'\<sharp>(trm{coname:=(y).Q},Q)")
 apply(erule exE)
 apply(simp add: fresh_prod)
 apply(erule conjE)+
 apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)

 done
 
 lemma not_Ax2:
   shows "\<not>(x\<sharp>M) \<Longrightarrow> M{x:=<b>.Q} \<noteq> Ax y a"
 apply(nominal_induct M avoiding: b y Q x a rule: trm.strong_induct)
-apply(auto simp add: fresh_atm abs_fresh abs_supp fin_supp)
+apply(auto simp: fresh_atm abs_fresh abs_supp fin_supp)
 apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<b>.Q},Q)")
 apply(erule exE)
 apply(simp add: fresh_prod)
 apply(erule conjE)+
 apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)

   shows "N{y:=<c>.P}{x:=<c>.P} = N{x:=<c>.Ax y c}{y:=<c>.P}"
 using a
 proof(nominal_induct N avoiding: x y c P rule: trm.strong_induct)
   case Ax
   then show ?case
-    by (auto simp add: abs_fresh fresh_atm forget trm.inject)
+    by (auto simp: abs_fresh fresh_atm forget trm.inject)
 next 
   case (Cut d M u M' x' y' c P)
   with assms show ?case
     apply(simp)
     apply(auto)

     apply(simp add: not_Ax2)
     done
 next
   case NotR
   then show ?case
-    by (auto simp add: abs_fresh fresh_atm forget)
+    by (auto simp: abs_fresh fresh_atm forget)
 next
   case (NotL d M u)
   then show ?case
-    apply (auto simp add: abs_fresh fresh_atm forget)
+    apply (auto simp: abs_fresh fresh_atm forget)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},y,x)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_NotL)
     apply(rule trans)
     apply(rule better_Cut_substn)
     apply(simp add: abs_fresh)
     apply(simp)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(simp add: trm.inject alpha forget)
     apply(rule exists_fresh'(1)[OF fs_name1])
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},Ax y c,y,x)")
     apply(erule exE, simp only: fresh_prod)
     apply(erule conjE)+

     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (AndR d1 M d2 M' d3)
   then show ?case
-    by (auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
 next
   case (AndL1 u M d)
   then show ?case
-    apply(auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndL1)
     apply(rule trans)
     apply(rule better_Cut_substn)
     apply(simp add: abs_fresh)
     apply(simp)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(simp add: trm.inject alpha forget)
     apply(rule exists_fresh'(1)[OF fs_name1])
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)")
     apply(erule exE, simp only: fresh_prod)
     apply(erule conjE)+

     apply(rule trans)
     apply(rule better_Cut_substn)
     apply(simp add: abs_fresh)
     apply(simp)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (AndL2 u M d)
   then show ?case
-    apply(auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndL2)
     apply(rule trans)
     apply(rule better_Cut_substn)
     apply(simp add: abs_fresh)
     apply(simp)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(simp add: trm.inject alpha forget)
     apply(rule exists_fresh'(1)[OF fs_name1])
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,Ax y c,M{x:=<c>.Ax y c},M{x:=<c>.Ax y c}{y:=<c>.P},u,y,x)")
     apply(erule exE, simp only: fresh_prod)
     apply(erule conjE)+

     apply(rule trans)
     apply(rule better_Cut_substn)
     apply(simp add: abs_fresh)
     apply(simp)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case OrR1
   then show ?case
-    by (auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
 next
   case OrR2
   then show ?case
-    by (auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
 next
   case (OrL x1 M x2 M' x3)
   then show ?case
-    apply(auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{y:=<c>.P},M{x:=<c>.Ax y c}{y:=<c>.P},
                                         M'{y:=<c>.P},M'{x:=<c>.Ax y c}{y:=<c>.P},x1,x2,x3,y,x)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_OrL)
     apply(rule trans)
     apply(rule better_Cut_substn)
     apply(simp add: abs_fresh)
     apply(simp)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(simp add: trm.inject alpha forget)
     apply(rule trans)
     apply(rule substn.simps)
     apply(simp add: abs_fresh subst_fresh fresh_atm)
     apply(simp add: abs_fresh subst_fresh fresh_atm)

     apply(rule substn.simps)
     apply(simp add: abs_fresh subst_fresh fresh_atm)
     apply(simp add: abs_fresh subst_fresh fresh_atm)
     apply(force)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case ImpR
   then show ?case
-    by (auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
 next
   case (ImpL a M x1 M' x2)
   then show ?case
-    apply(auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{x2:=<c>.P},M{x:=<c>.Ax x2 c}{x2:=<c>.P},
                                         M'{x2:=<c>.P},M'{x:=<c>.Ax x2 c}{x2:=<c>.P},x1,y,x)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_ImpL)
     apply(rule trans)
     apply(rule better_Cut_substn)
     apply(simp add: abs_fresh)
     apply(simp)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(simp add: trm.inject alpha forget)
     apply(rule trans)
     apply(rule substn.simps)
     apply(simp add: abs_fresh subst_fresh fresh_atm)
     apply(simp add: abs_fresh subst_fresh fresh_atm)

     apply(rule trans)
     apply(rule substn.simps)
     apply(simp add: abs_fresh subst_fresh fresh_atm)
     apply(simp add: abs_fresh subst_fresh fresh_atm)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 qed 
 
 lemma interesting_subst1':

   shows "N{a:=(y).P}{b:=(y).P} = N{b:=(y).Ax y a}{a:=(y).P}"
 using a
 proof(nominal_induct N avoiding: a b y P rule: trm.strong_induct)
   case Ax
   then show ?case
-    by (auto simp add: abs_fresh fresh_atm forget trm.inject)
+    by (auto simp: abs_fresh fresh_atm forget trm.inject)
 next 
   case (Cut d M u M' x' y' c P)
   with assms show ?case
     apply(simp)
-    apply(auto simp add: trm.inject)
+    apply(auto simp: trm.inject)
     apply(rule trans)
     apply(rule better_Cut_substc)
     apply(simp)
     apply(simp add: abs_fresh)
     apply(simp add: forget)

     apply(simp add: not_Ax1)
     done
 next
   case NotL
   then show ?case
-    by (auto simp add: abs_fresh fresh_atm forget)
+    by (auto simp: abs_fresh fresh_atm forget)
 next
   case (NotR u M d)
   then show ?case
-    apply (auto simp add: abs_fresh fresh_atm forget)
+    apply (auto simp: abs_fresh fresh_atm forget)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(b,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P},u,y)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_NotR)
     apply(rule trans)
     apply(rule better_Cut_substc)
     apply(simp add: abs_fresh)
     apply(simp add: abs_fresh)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(simp add: trm.inject alpha forget)
     apply(rule exists_fresh'(2)[OF fs_coname1])
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(P,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P},Ax y a,y,d)")
     apply(erule exE, simp only: fresh_prod)
     apply(erule conjE)+

     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (AndR d1 M d2 M' d3)
   then show ?case
-    apply(auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(P,M{d3:=(y).P},M{b:=(y).Ax y d3}{d3:=(y).P},
                                         M'{d3:=(y).P},M'{b:=(y).Ax y d3}{d3:=(y).P},d1,d2,d3,b,y)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndR)
     apply(rule trans)
     apply(rule better_Cut_substc)
     apply(simp add: abs_fresh fresh_atm)
     apply(simp add: abs_fresh fresh_atm)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(simp add: trm.inject alpha forget)
     apply(rule trans)
     apply(rule substc.simps)
     apply(simp add: abs_fresh subst_fresh fresh_atm)
     apply(simp add: abs_fresh subst_fresh fresh_atm)

     apply(rule substc.simps)
     apply(simp add: abs_fresh subst_fresh fresh_atm)
     apply(simp add: abs_fresh subst_fresh fresh_atm)
     apply(force)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (AndL1 u M d)
   then show ?case
-    by (auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
 next
   case (AndL2 u M d)
   then show ?case
-    by (auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
 next
   case (OrR1 d M e)
   then show ?case
-    apply (auto simp add: abs_fresh fresh_atm forget)
+    apply (auto simp: abs_fresh fresh_atm forget)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(b,P,M{e:=(y).P},M{b:=(y).Ax y e}{e:=(y).P},d,e)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_OrR1)
     apply(rule trans)
     apply(rule better_Cut_substc)
     apply(simp add: abs_fresh)
     apply(simp add: abs_fresh)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(simp add: trm.inject alpha forget)
     apply(rule exists_fresh'(2)[OF fs_coname1])
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)")
     apply(erule exE, simp only: fresh_prod)
     apply(erule conjE)+

     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (OrR2 d M e)
   then show ?case
-    apply (auto simp add: abs_fresh fresh_atm forget)
+    apply (auto simp: abs_fresh fresh_atm forget)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(b,P,M{e:=(y).P},M{b:=(y).Ax y e}{e:=(y).P},d,e)")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_OrR2)
     apply(rule trans)
     apply(rule better_Cut_substc)
     apply(simp add: abs_fresh)
     apply(simp add: abs_fresh)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(simp add: trm.inject alpha forget)
     apply(rule exists_fresh'(2)[OF fs_coname1])
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(b,P,Ax y a,M{e:=(y).Ax y a},M{e:=(y).Ax y a}{a:=(y).P},d,e)")
     apply(erule exE, simp only: fresh_prod)
     apply(erule conjE)+

     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (OrL x1 M x2 M' x3)
   then show ?case
-    by(auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    by(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
 next
   case ImpL
   then show ?case
-    by (auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    by (auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
 next
   case (ImpR u e M d)
   then show ?case
-    apply(auto simp add: abs_fresh fresh_atm forget trm.inject subst_fresh)
+    apply(auto simp: abs_fresh fresh_atm forget trm.inject subst_fresh)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(b,e,d,P,M{d:=(y).P},M{b:=(y).Ax y d}{d:=(y).P})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_ImpR)
     apply(rule trans)
     apply(rule better_Cut_substc)
     apply(simp add: abs_fresh)
     apply(simp add: abs_fresh)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(simp add: trm.inject alpha forget)
     apply(rule exists_fresh'(2)[OF fs_coname1])
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(e,d,P,Ax y a,M{d:=(y).Ax y a},M{d:=(y).Ax y a}{a:=(y).P})")
     apply(erule exE, simp only: fresh_prod)
     apply(erule conjE)+

     apply(rule trans)
     apply(rule substc.simps)
     apply(simp add: abs_fresh subst_fresh fresh_atm)
     apply(simp add: abs_fresh subst_fresh fresh_atm)
     apply(simp)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 qed 
 
 lemma interesting_subst2':

     have "(Ax x b){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (x).Ax x b){b:=(y).Q}" using fs by simp
     also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).Q"
       using fs by (simp_all add: fresh_prod fresh_atm)
     also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).(Q{x:=<a>.(P{b:=(y).Q})})" using fs by (simp add: forget)
     also have "\<dots> = (Cut <b>.Ax x b (y).Q){x:=<a>.(P{b:=(y).Q})}"
-      using fs asm by (auto simp add: fresh_prod fresh_atm subst_fresh)
+      using fs asm by (auto simp: fresh_prod fresh_atm subst_fresh)
     also have "\<dots> = (Ax x b){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" using fs by simp
     finally have "(Ax z c){x:=<a>.P}{b:=(y).Q} = (Ax z c){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" 
       using asm by simp
   }
   moreover

     have "(Ax z c){x:=<a>.P}{b:=(y).Q} = (Ax z c){b:=(y).Q}" using asm by simp
     also have "\<dots> = Cut <b>.Ax z c (y).Q" using fs asm by simp
     also have "\<dots> = Cut <b>.(Ax z c{x:=<a>.(P{b:=(y).Q})}) (y).(Q{x:=<a>.(P{b:=(y).Q})})" 
       using fs asm by (simp add: forget)
     also have "\<dots> = (Cut <b>.Ax z c (y).Q){x:=<a>.(P{b:=(y).Q})}" using asm fs
-      by (auto simp add: trm.inject subst_fresh fresh_prod fresh_atm abs_fresh)
+      by (auto simp: trm.inject subst_fresh fresh_prod fresh_atm abs_fresh)
     also have "\<dots> = (Ax z c){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" using asm fs by simp
     finally have "(Ax z c){x:=<a>.P}{b:=(y).Q} = (Ax z c){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" by simp
   }
   moreover
   { assume asm: "z=x \<and> c\<noteq>b"
     have "(Ax z c){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (x).Ax z c){b:=(y).Q}" using fs asm by simp
-    also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (x).Ax z c" using fs asm by (auto simp add: trm.inject abs_fresh)
+    also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (x).Ax z c" using fs asm by (auto simp: trm.inject abs_fresh)
     also have "\<dots> = (Ax z c){x:=<a>.(P{b:=(y).Q})}" using fs asm by simp
     also have "\<dots> = (Ax z c){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" using asm by auto
     finally have "(Ax z c){x:=<a>.P}{b:=(y).Q} = (Ax z c){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" by simp
   }
   moreover

   case (Cut c M z N)
   { assume asm: "M = Ax x c \<and> N = Ax z b"
     have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <a>.P (z).(N{x:=<a>.P})){b:=(y).Q}" 
       using Cut asm by simp
     also have "\<dots> = (Cut <a>.P (z).N){b:=(y).Q}" using Cut asm by (simp add: fresh_atm)
-    also have "\<dots> = (Cut <a>.(P{b:=(y).Q}) (y).Q)" using Cut asm by (auto simp add: fresh_prod fresh_atm)
+    also have "\<dots> = (Cut <a>.(P{b:=(y).Q}) (y).Q)" using Cut asm by (auto simp: fresh_prod fresh_atm)
     finally have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <a>.(P{b:=(y).Q}) (y).Q)" by simp
     have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} = (Cut <c>.M (y).Q){x:=<a>.(P{b:=(y).Q})}"
       using Cut asm by (simp add: fresh_atm)
     also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).(Q{x:=<a>.(P{b:=(y).Q})})" using Cut asm
-      by (auto simp add: fresh_prod fresh_atm subst_fresh)
+      by (auto simp: fresh_prod fresh_atm subst_fresh)
     also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (y).Q" using Cut asm by (simp add: forget)
     finally have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} = Cut <a>.(P{b:=(y).Q}) (y).Q"
       by simp
     have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" 
       using eq1 eq2 by simp

     have eq1: "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = Cut <c>.(M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}}) (y).Q" 
       by simp
     have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} = 
                (Cut <c>.(M{b:=(y).Q}) (y).Q){x:=<a>.(P{b:=(y).Q})}" using Cut asm by simp
     also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).(Q{x:=<a>.(P{b:=(y).Q})})"
-      using Cut asm neq by (auto simp add: fresh_prod fresh_atm subst_fresh abs_fresh)
+      using Cut asm neq by (auto simp: fresh_prod fresh_atm subst_fresh abs_fresh)
     also have "\<dots> = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).Q" using Cut asm by (simp add: forget)
     finally have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} 
                                        = Cut <c>.(M{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}) (y).Q" by simp
     have "(Cut <c>.M (z).N){x:=<a>.P}{b:=(y).Q} = (Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})}" 
       using eq1 eq2 by simp

                     = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" by simp
     have "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} 
                     = (Cut <c>.(M{b:=(y).Q}) (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}"
       using Cut asm by auto
     also have "\<dots> = (Cut <c>.M (z).(N{b:=(y).Q})){x:=<a>.(P{b:=(y).Q})}"
-      using Cut asm by (auto simp add: fresh_atm)
+      using Cut asm by (auto simp: fresh_atm)
     also have "\<dots> = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" 
       using Cut asm by (simp add: fresh_prod fresh_atm subst_fresh)
     finally 
     have eq2: "(Cut <c>.M (z).N){b:=(y).Q}{x:=<a>.(P{b:=(y).Q})} 
          = Cut <a>.(P{b:=(y).Q}) (z).(N{b:=(y).Q}{x:=<a>.(P{b:=(y).Q})})" by simp

   }
   ultimately show ?case by blast
 next
   case (NotR z M c)
   then show ?case
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(M{c:=(y).Q},M{c:=(y).Q}{x:=<a>.P{c:=(y).Q}},Q,a,P,c,y)")
     apply(erule exE)
     apply(simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_NotR abs_fresh fresh_atm)

     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (NotL c M z)
   then show ?case  
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{x:=<a>.P},P{b:=(y).Q},M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},y,Q)")
     apply(erule exE)
     apply(simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_NotL abs_fresh fresh_atm)
     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (AndR c1 M c2 N c3)
   then show ?case  
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(Q,M{c3:=(y).Q},M{c3:=(y).Q}{x:=<a>.P{c3:=(y).Q}},c2,c3,a,
                                      P{c3:=(y).Q},N{c3:=(y).Q},N{c3:=(y).Q}{x:=<a>.P{c3:=(y).Q}},c1)")
     apply(erule exE)
     apply(simp add: fresh_prod)
     apply(erule conjE)+

     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (AndL1 z1 M z2)
   then show ?case  
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{x:=<a>.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}})")
     apply(erule exE)
     apply(simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndL1 abs_fresh fresh_atm)
     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (AndL2 z1 M z2)
   then show ?case  
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{x:=<a>.P},P{b:=(y).Q},z1,y,Q,M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}})")
     apply(erule exE)
     apply(simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndL2 abs_fresh fresh_atm)
     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (OrL z1 M z2 N z3)
   then show ?case  
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,M{x:=<a>.P},M{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},z2,z3,a,y,Q,
                                      P{b:=(y).Q},N{x:=<a>.P},N{b:=(y).Q}{x:=<a>.P{b:=(y).Q}},z1)")
     apply(erule exE)
     apply(simp add: fresh_prod)
     apply(erule conjE)+

     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (OrR1 c1 M c2)
   then show ?case  
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(Q,M{c2:=(y).Q},a,P{c2:=(y).Q},c1,
                                                      M{c2:=(y).Q}{x:=<a>.P{c2:=(y).Q}})")
     apply(erule exE)
     apply(simp add: fresh_prod)
     apply(erule conjE)+

     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (OrR2 c1 M c2)
   then show ?case  
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(Q,M{c2:=(y).Q},a,P{c2:=(y).Q},c1,
                                                      M{c2:=(y).Q}{x:=<a>.P{c2:=(y).Q}})")
     apply(erule exE)
     apply(simp add: fresh_prod)
     apply(erule conjE)+

     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (ImpR z c M d)
   then show ?case  
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(Q,M{d:=(y).Q},a,P{d:=(y).Q},c,
                                                      M{d:=(y).Q}{x:=<a>.P{d:=(y).Q}})")
     apply(erule exE)
     apply(simp add: fresh_prod)
     apply(erule conjE)+

     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (ImpL c M z N u)
   then show ?case  
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)
     apply(subgoal_tac "\<exists>z'::name. z'\<sharp>(P,P{b:=(y).Q},M{u:=<a>.P},N{u:=<a>.P},y,Q,
                         M{b:=(y).Q}{u:=<a>.P{b:=(y).Q}},N{b:=(y).Q}{u:=<a>.P{b:=(y).Q}},z)")
     apply(erule exE)
     apply(simp add: fresh_prod)
     apply(erule conjE)+

   shows "M{a:=(x).N}{y:=<b>.P} = M{y:=<b>.P}{a:=(x).N{y:=<b>.P}}"
 using a
 proof(nominal_induct M avoiding: a x N y b P rule: trm.strong_induct)
   case (Ax z c)
   then show ?case
-    by (auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
+    by (auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
 next
   case (Cut d M' u M'')
   then show ?case
     apply(simp add: fresh_atm fresh_prod trm.inject abs_fresh)
     apply(auto)

     apply(simp add: not_Ax2)
     done
 next
   case (NotR z M' d) 
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(y,P,N,N{y:=<b>.P},M'{d:=(x).N},M'{y:=<b>.P}{d:=(x).N{y:=<b>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_NotR)
     apply(rule trans)

     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (NotL d M' z) 
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(z,y,P,N,N{y:=<b>.P},M'{y:=<b>.P},M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_NotL)
     apply(rule sym)

     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (AndR d M' e M'' f) 
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
     apply(subgoal_tac "\<exists>a'::coname. a'\<sharp>(P,b,d,e,N,N{y:=<b>.P},M'{f:=(x).N},M''{f:=(x).N},
                   M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}},M''{y:=<b>.P}{f:=(x).N{y:=<b>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndR)

     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (AndL1 z M' u) 
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,b,z,u,x,N,M'{y:=<b>.P},M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndL1)
     apply(rule sym)

     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (AndL2 z M' u) 
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(P,b,z,u,x,N,M'{y:=<b>.P},M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndL2)
     apply(rule sym)

     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (OrL u M' v M'' w) 
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
     apply(subgoal_tac "\<exists>z'::name. z'\<sharp>(P,b,u,w,v,N,N{y:=<b>.P},M'{y:=<b>.P},M''{y:=<b>.P},
                   M'{y:=<b>.P}{a:=(x).N{y:=<b>.P}},M''{y:=<b>.P}{a:=(x).N{y:=<b>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_OrL)

     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (OrR1 e M' f) 
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
     apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(P,b,e,f,x,N,N{y:=<b>.P},
                                         M'{f:=(x).N},M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_OrR1)

     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (OrR2 e M' f) 
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
     apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(P,b,e,f,x,N,N{y:=<b>.P},
                                         M'{f:=(x).N},M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_OrR2)

     apply(rule exists_fresh'(2)[OF fs_coname1])
     done
 next
   case (ImpR x e M' f) 
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
     apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(P,b,e,f,x,N,N{y:=<b>.P},
                                         M'{f:=(x).N},M'{y:=<b>.P}{f:=(x).N{y:=<b>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_ImpR)

     apply(simp add: fresh_atm trm.inject alpha abs_fresh fin_supp abs_supp)
     done
 next
   case (ImpL e M' v M'' w) 
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget trm.inject)
     apply(subgoal_tac "\<exists>z'::name. z'\<sharp>(P,b,e,w,v,N,N{y:=<b>.P},M'{w:=<b>.P},M''{w:=<b>.P},
                   M'{w:=<b>.P}{a:=(x).N{w:=<b>.P}},M''{w:=<b>.P}{a:=(x).N{w:=<b>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_ImpL)

   shows "N{x:=<a>.M}{y:=<c>.P} = N{y:=<c>.P}{x:=<a>.(M{y:=<c>.P})}"
 using a
 proof(nominal_induct N avoiding: x y a c M P rule: trm.strong_induct)
   case (Ax z c)
   then show ?case
-    by(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
 next
   case (Cut d M' u M'')
   then show ?case
     apply(simp add: fresh_atm fresh_prod trm.inject abs_fresh)
     apply(auto)

     apply(simp add: not_Ax2)
     done
 next
   case NotR
   then show ?case
-    by(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
 next
   case (NotL d M' u)
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(y,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_NotL)
     apply(rule trans)

     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case AndR
   then show ?case
-    by(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
 next
   case (AndL1 u M' v)
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(u,y,v,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndL1)
     apply(rule trans)

     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case (AndL2 u M' v)
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(u,y,v,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_AndL2)
     apply(rule trans)

     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case OrR1
   then show ?case
-    by(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
 next
   case OrR2
   then show ?case
-    by(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
 next
   case (OrL x1 M' x2 M'' x3)
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(y,P,M,M{y:=<c>.P},M'{x:=<a>.M},M'{y:=<c>.P}{x:=<a>.M{y:=<c>.P}},
                                       x1,x2,x3,M''{x:=<a>.M},M''{y:=<c>.P}{x:=<a>.M{y:=<c>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_OrL)

     apply(rule exists_fresh'(1)[OF fs_name1])
     done
 next
   case ImpR
   then show ?case
-    by(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
 next
   case (ImpL d M' x1 M'' x2)
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(y,P,M,M{y:=<c>.P},M'{x2:=<a>.M},M'{y:=<c>.P}{x2:=<a>.M{y:=<c>.P}},
                                       x1,x2,M''{x2:=<a>.M},M''{y:=<c>.P}{x2:=<a>.M{y:=<c>.P}})")
     apply(erule exE, simp add: fresh_prod)
     apply(erule conjE)+
     apply(simp add: fresh_fun_simp_ImpL)

   shows "N{a:=(x).M}{c:=(y).P} = N{c:=(y).P}{a:=(x).(M{c:=(y).P})}"
 using a
 proof(nominal_induct N avoiding: x y a c M P rule: trm.strong_induct)
   case (Ax z c)
   then show ?case
-    by (auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    by (auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
 next
   case (Cut d M' u M'')
   then show ?case
     apply(simp add: fresh_atm fresh_prod trm.inject abs_fresh)
     apply(auto)

     apply(simp add: not_Ax1)
     done
 next
   case NotL
   then show ?case
-    by(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
 next
   case (NotR u M' d)
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
     apply(simp add: abs_fresh subst_fresh)
     apply(rule trans)

     apply(simp)
     apply(simp add: trm.inject alpha)
     apply(rule trans)
     apply(rule substc.simps)
     apply(simp add: fresh_prod fresh_atm)
-    apply(auto simp add: fresh_atm fresh_prod)[1]
+    apply(auto simp: fresh_atm fresh_prod)[1]
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
     apply(rule sym)
     apply(rule trans)
     apply(rule better_Cut_substc)
     apply(simp add: fresh_prod fresh_atm subst_fresh)
     apply(simp add: abs_fresh subst_fresh)
-    apply(auto simp add: fresh_atm)
+    apply(auto simp: fresh_atm)
     apply(simp add: trm.inject alpha forget)
     apply(rule trans)
     apply(rule substc.simps)
     apply(simp add: fresh_atm subst_fresh)
-    apply(auto simp add: fresh_prod fresh_atm) 
+    apply(auto simp: fresh_prod fresh_atm) 
     done
 next
   case AndL1
   then show ?case
-    by(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
 next
   case AndL2
   then show ?case
-    by(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
 next
   case (AndR d M e M' f)
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
     apply(simp add: abs_fresh subst_fresh)
     apply(rule trans)

     apply(simp add: abs_fresh)
     apply(simp)
     apply(simp add: trm.inject alpha)
     apply(rule trans)
     apply(rule substc.simps)
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
-    apply(simp)
-    apply(auto simp add: fresh_atm fresh_prod)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+    apply(simp)
+    apply(auto simp: fresh_atm fresh_prod)[1]
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
     apply(rule sym)
     apply(rule trans)
     apply(rule better_Cut_substc)
     apply(simp add: subst_fresh fresh_atm fresh_prod)
     apply(simp add: abs_fresh subst_fresh)
-    apply(auto simp add: fresh_atm)[1]
+    apply(auto simp: fresh_atm)[1]
     apply(simp add: trm.inject alpha forget)
     apply(rule trans)
     apply(rule substc.simps)
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
-    apply(simp)
-    apply(auto simp add: fresh_atm fresh_prod)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+    apply(simp)
+    apply(auto simp: fresh_atm fresh_prod)[1]
     done
 next
   case OrL
   then show ?case
-    by(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
 next
   case (OrR1 d M' e)
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
     apply(simp add: abs_fresh subst_fresh)
     apply(rule trans)

     apply(simp add: abs_fresh)
     apply(simp)
     apply(simp add: trm.inject alpha)
     apply(rule trans)
     apply(rule substc.simps)
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
     apply(rule sym)
     apply(rule trans)
     apply(rule better_Cut_substc)
     apply(simp add: subst_fresh fresh_atm fresh_prod)
     apply(simp add: abs_fresh subst_fresh)
-    apply(auto simp add: fresh_atm)[1]
+    apply(auto simp: fresh_atm)[1]
     apply(simp add: trm.inject alpha forget)
     apply(rule trans)
     apply(rule substc.simps)
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
     done
 next
   case (OrR2 d M' e)
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
     apply(simp add: abs_fresh subst_fresh)
     apply(rule trans)

     apply(simp add: abs_fresh)
     apply(simp)
     apply(simp add: trm.inject alpha)
     apply(rule trans)
     apply(rule substc.simps)
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
     apply(rule sym)
     apply(rule trans)
     apply(rule better_Cut_substc)
     apply(simp add: subst_fresh fresh_atm fresh_prod)
     apply(simp add: abs_fresh subst_fresh)
-    apply(auto simp add: fresh_atm)[1]
+    apply(auto simp: fresh_atm)[1]
     apply(simp add: trm.inject alpha forget)
     apply(rule trans)
     apply(rule substc.simps)
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
     done
 next
   case ImpL
   then show ?case
-    by(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    by(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
 next
   case (ImpR u d M' e)
   then show ?case
-    apply(auto simp add: subst_fresh abs_fresh fresh_atm fresh_prod forget)
+    apply(auto simp: subst_fresh abs_fresh fresh_atm fresh_prod forget)
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
     apply(simp add: abs_fresh subst_fresh)
     apply(rule trans)

     apply(simp add: abs_fresh)
     apply(simp)
     apply(simp add: trm.inject alpha)
     apply(rule trans)
     apply(rule substc.simps)
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)[1]
     apply(generate_fresh "coname")
     apply(fresh_fun_simp)
     apply(fresh_fun_simp)
     apply(rule sym)
     apply(rule trans)
     apply(rule better_Cut_substc)
     apply(simp add: subst_fresh fresh_atm fresh_prod)
     apply(simp add: abs_fresh subst_fresh)
-    apply(auto simp add: fresh_atm)[1]
+    apply(auto simp: fresh_atm)[1]
     apply(simp add: trm.inject alpha forget)
     apply(rule trans)
     apply(rule substc.simps)
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh)[1]
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)[1]
-    apply(auto simp add: fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)[1]
+    apply(auto simp: fresh_prod fresh_atm subst_fresh abs_fresh abs_supp fin_supp)[1]
     done
 qed
 
 end