--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -12,10 +12,12 @@
     (M $$ N)* = Lam k (M* $$ Lam m (N* $$ Lam n (m~ $$ n~ $$ k~)))"
 unfolding eqvt_def CPS_graph_def
 apply (rule, perm_simp, rule, rule)
+using [[simproc del: alpha_lst]]
 apply (simp_all add: fresh_Pair_elim)
 apply (rule_tac y="x" in lt.exhaust)
 apply (auto)[3]
 apply (rule_tac x="name" and ?'a="name" in obtain_fresh)
+using [[simproc del: alpha_lst]]
 apply (simp_all add: fresh_at_base)[3]
 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh)
 apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh)
@@ -81,6 +83,7 @@
   unfolding convert_graph_def eqvt_def
   apply (rule, perm_simp, rule, rule)
   apply (erule lt.exhaust)
+  using [[simproc del: alpha_lst]]
   apply (simp_all)
   apply blast
   apply (simp add: Abs1_eq_iff CPS.eqvt)
@@ -113,6 +116,7 @@
     Kapply (M $$ N) K = M; (Lam m (N*  $$ (Lam n (Var m $$ Var n $$ K))))"
   unfolding Kapply_graph_def eqvt_def
   apply (rule, perm_simp, rule, rule)
+using [[simproc del: alpha_lst]]
 apply (simp_all)
 apply (case_tac x)
 apply (rule_tac y="a" in lt.exhaust)

--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -18,8 +18,10 @@
 | fill_abs  : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Lam x (C<M>)"
   unfolding eqvt_def fill_graph_def
   apply perm_simp
+  using [[simproc del: alpha_lst]]
   apply auto
   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
+  using [[simproc del: alpha_lst]]
   apply (auto simp add: fresh_star_def)
   apply (erule Abs_lst1_fcb)
   apply (simp_all add: Abs_fresh_iff)[2]
@@ -41,8 +43,10 @@
 | "ccomp (CFun C N) C'  = CFun (ccomp C C') N"
   unfolding eqvt_def ccomp_graph_def
   apply perm_simp
+  using [[simproc del: alpha_lst]]
   apply auto
   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
+  using [[simproc del: alpha_lst]]
   apply (auto simp add: fresh_star_def)
   apply blast+
   apply (erule Abs_lst1_fcb)
@@ -71,10 +75,12 @@
      ccomp (CPS M) (CAbs a (CArg (Var a $$ (CPSv N)) Hole))"
 | "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $$ N) =
      ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $$ Var b) Hole))))"
+  using [[simproc del: alpha_lst]]
   apply auto
   defer
   apply (case_tac x)
   apply (rule_tac y="a" in lt.exhaust)
+  using [[simproc del: alpha_lst]]
   apply auto
   apply blast
   apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)

--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -15,6 +15,7 @@
 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))"
   apply (simp only: eqvt_def CPS1_CPS2_graph_def)
   apply (rule, perm_simp, rule)
+  using [[simproc del: alpha_lst]]
   apply auto
   apply (case_tac x)
   apply (case_tac a)

--- a/Nominal/Ex/CPS/Lt.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/CPS/Lt.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -19,6 +19,7 @@
   unfolding eqvt_def subst_graph_def
   apply (simp)
   apply(rule TrueI)
+  using [[simproc del: alpha_lst]]
   apply(auto simp add: lt.distinct lt.eq_iff)
   apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)
   apply blast
@@ -60,7 +61,7 @@
 inductive
   eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
   where
-   evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $$ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])"
+   evbeta: "\<lbrakk>atom x \<sharp> V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $$ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])"
 |  ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $$ M) \<longrightarrow>\<^isub>\<beta> (V $$ M')"
 |  ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $$ N) \<longrightarrow>\<^isub>\<beta> (M' $$ N)"
 

--- a/Nominal/Ex/Classical.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/Classical.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -77,6 +77,7 @@
   apply(metis)+
   -- "compatibility"
   apply(all_trivials)
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply(rule conjI)
   apply(elim conjE)
@@ -280,6 +281,7 @@
   apply (simp_all add: fresh_star_def)[12]
   apply(metis)+
   -- "compatibility"
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply(rule conjI)
   apply(elim conjE)
@@ -479,18 +481,7 @@
   apply(case_tac x)
   apply(rule_tac y="a" and c="(b, c, d)" in trm.strong_exhaust)
   apply (simp_all add: fresh_star_def fresh_Pair)[12]
-  apply(metis)+
-  apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)")
-  apply(auto simp add: fresh_Pair)[1]
-  apply(metis)+
-  apply(subgoal_tac "\<exists>x'::name. atom x' \<sharp> (trm, b, d)")
-  apply(auto simp add: fresh_Pair)[1]
-  apply(rule obtain_fresh)
-  apply(auto)[1]
-  apply(metis)+
-  -- "compatibility"
-  apply(all_trivials)
-  apply(simp)
+  apply(metis)
   oops
 
 end

--- a/Nominal/Ex/Lambda.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/Lambda.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -94,6 +94,7 @@
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
 apply(auto)[3]
+using [[simproc del: alpha_lst]]
 apply(simp_all)
 apply(erule_tac c="()" in Abs_lst1_fcb2')
 apply(simp_all add: pure_fresh fresh_star_def)[3]
@@ -124,6 +125,7 @@
 apply(case_tac x)
 apply(rule_tac y="b" and c="a" in lam.strong_exhaust)
 apply(auto simp add: fresh_star_def)[3]
+using [[simproc del: alpha_lst]]
 apply(simp_all)
 apply(erule conjE)+
 apply(erule_tac Abs_lst1_fcb2)
@@ -169,6 +171,7 @@
   apply(case_tac x)
   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)
   apply(auto simp add: fresh_star_def)[3]
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply(erule conjE)+
   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
@@ -202,6 +205,7 @@
 apply(simp)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
+using [[simproc del: alpha_lst]]
 apply(auto)
 apply (erule_tac c="()" in Abs_lst1_fcb2)
 apply(simp add: supp_removeAll fresh_def)
@@ -229,6 +233,7 @@
   apply(auto)[9]
   apply(rule_tac y="x" in lam.exhaust)
   apply(auto)[3]
+  using [[simproc del: alpha_lst]]
   apply(simp)
   apply(erule_tac c="()" in Abs_lst1_fcb2)
   apply(simp add: fresh_minus_atom_set)
@@ -254,6 +259,7 @@
   apply(simp add: eqvt_def height_graph_def)
   apply(rule TrueI)
   apply(rule_tac y="x" in lam.exhaust)
+  using [[simproc del: alpha_lst]]
   apply(auto)
   apply (erule_tac c="()" in Abs_lst1_fcb2)
   apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
@@ -276,9 +282,11 @@
   unfolding eqvt_def subst_graph_def
   apply(simp)
   apply(rule TrueI)
+  using [[simproc del: alpha_lst]]
   apply(auto)
   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
   apply(blast)+
+  using [[simproc del: alpha_lst]]
   apply(simp_all add: fresh_star_def fresh_Pair_elim)
   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
   apply(simp_all add: Abs_fresh_iff)
@@ -306,8 +314,10 @@
 text {* same lemma but with subst.induction *}
 lemma forget2:
   shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
-  by (induct t x s rule: subst.induct)
-     (auto simp add:  fresh_at_base fresh_Pair)
+  apply(induct t x s rule: subst.induct)
+  using [[simproc del: alpha_lst]]
+  apply(auto simp add:  flip_fresh_fresh fresh_Pair fresh_at_base)
+  done
 
 lemma fresh_fact:
   fixes z::"name"
@@ -467,6 +477,7 @@
   apply(auto)[1]
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply (auto simp add: fresh_star_def)[3]
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply(erule conjE)+
   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
@@ -498,6 +509,7 @@
   apply(auto)[3]
   apply(all_trivials)
   apply(simp)
+  using [[simproc del: alpha_lst]]
   apply(simp)
   apply(erule_tac c="()" in Abs_lst1_fcb2')
   apply(simp add: pure_fresh)
@@ -526,6 +538,7 @@
   apply(all_trivials)
   apply(simp)
   apply(simp)
+  using [[simproc del: alpha_lst]]
   apply(simp)
   apply(erule conjE)
   apply(erule Abs_lst1_fcb2')
@@ -582,6 +595,7 @@
   apply (case_tac x)
   apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
   apply (auto simp add: fresh_star_def fresh_at_list)[3]
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply(elim conjE)
   apply (erule_tac c="xsa" in Abs_lst1_fcb2')
@@ -641,6 +655,7 @@
   apply(rule TrueI)
   apply (case_tac x)
   apply (case_tac a rule: lam.exhaust)
+  using [[simproc del: alpha_lst]]
   apply simp_all[3]
   apply blast
   apply (case_tac b)
@@ -649,6 +664,7 @@
   apply blast
   apply blast
   apply (simp add: Abs1_eq_iff fresh_star_def)
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply(erule_tac c="()" in Abs_lst1_fcb2)
   apply (simp add: Abs_fresh_iff)
@@ -692,6 +708,7 @@
 apply (rule TrueI)
 apply (case_tac x)
 apply (rule_tac y="a" in lam.exhaust)
+using [[simproc del: alpha_lst]]
 apply simp_all
 apply blast
 apply blast
@@ -718,6 +735,7 @@
   apply (simp add: eqvt_def map_term_graph_def)
   apply(rule TrueI)
   apply (case_tac x, case_tac "eqvt a", case_tac b rule: lam.exhaust)
+  using [[simproc del: alpha_lst]]
   apply auto
   apply (erule Abs_lst1_fcb)
   apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app)
@@ -890,13 +908,16 @@
   apply(rule_tac y="b" in lam.exhaust)
   apply(auto)[3]
   apply(rule_tac y="b" and c="(name, lam)" in lam.strong_exhaust)
+  using [[simproc del: alpha_lst]]
   apply(auto)[3]
   apply(drule_tac x="name" in meta_spec)
   apply(drule_tac x="name" in meta_spec)
   apply(drule_tac x="lam" in meta_spec)
   apply(drule_tac x="(name \<leftrightarrow> namea) \<bullet> lama" in meta_spec)
+  using [[simproc del: alpha_lst]]
   apply(simp add: Abs1_eq_iff fresh_star_def fresh_Pair_elim fresh_at_base flip_def)
   apply (metis Nominal2_Base.swap_commute fresh_permute_iff sort_of_atom_eq swap_atom_simps(2))
+  using [[simproc del: alpha_lst]]
   apply simp_all
   apply (simp add: abs_same_binder)
   apply (erule_tac c="()" in Abs_lst1_fcb2)

--- a/Nominal/Ex/Let.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/Let.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -122,6 +122,7 @@
   apply (drule_tac x="assn" in meta_spec)
   apply (drule_tac x="trm" in meta_spec)
   apply (simp add: alpha_bn_refl)
+  using [[simproc del: alpha_lst]]
   apply(simp_all)
   apply (erule_tac c="()" in Abs_lst1_fcb2)
   apply (simp_all add: pure_fresh fresh_star_def eqvt_at_def)[4]
@@ -179,6 +180,7 @@
   apply simp_all[7]
   prefer 2
   apply(simp)
+  using [[simproc del: alpha_lst]]
   apply(simp)
   apply(erule conjE)+
   apply (erule_tac c="(sa, ta)" in Abs_lst1_fcb2)

--- a/Nominal/Ex/LetRec.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/LetRec.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -39,9 +39,11 @@
 | "height_bp (Bp v t) = height_trm t"
   apply (simp only: eqvt_def height_trm_height_bp_graph_def)
   apply (rule, perm_simp, rule, rule TrueI)
+  using [[simproc del: alpha_set]]
   apply auto
   apply (case_tac x)
   apply (case_tac a rule: let_rec.exhaust(1))
+  using [[simproc del: alpha_set]]
   apply auto
   apply (case_tac b rule: let_rec.exhaust(2))
   apply blast

--- a/Nominal/Ex/Pi.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/Pi.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -179,6 +179,7 @@
 | "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}"
 | "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])"
 | "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>"
+  using [[simproc del: alpha_lst]]
   apply(auto simp add: piMix_distinct piMix_eq_iff)
   apply(subgoal_tac "\<And>p x r. subsGuard_mix_subsList_mix_subs_mix_graph x r \<Longrightarrow> subsGuard_mix_subsList_mix_subs_mix_graph (p \<bullet> x) (p \<bullet> r)")
   unfolding eqvt_def
@@ -294,10 +295,12 @@
   apply(case_tac ba)
   apply(simp)
   apply (rule_tac yb="a" and c="(bb,c)" in guardedTerm_mix_sumList_mix_piMix.strong_exhaust(3))
+  using [[simproc del: alpha_lst]]
   apply(auto simp add: fresh_star_def)[1]
   apply(blast)
   apply(blast)
   apply(blast)
+  using [[simproc del: alpha_lst]]
   apply(auto simp add: fresh_star_def)[1]
   apply(blast)
   apply(simp)

--- a/Nominal/Nominal2_Abs.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -801,7 +801,7 @@
 apply(blast)+
 done
 
-lemma Abs1_eq_fresh:
+lemma Abs1_eq_iff_fresh:
   fixes x y::"'a::fs"
   and a b c::"'b::at"
   assumes "atom c \<sharp> (a, b, x, y)"
@@ -843,7 +843,7 @@
     by (simp add: Abs1_eq)
 qed
 
-lemma Abs1_eq_all:
+lemma Abs1_eq_iff_all:
   fixes x y::"'a::fs"
   and z::"'c::fs"
   and a b::"'b::at"
@@ -852,25 +852,25 @@
   and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
 apply -
 apply(auto) 
-apply(simp add: Abs1_eq_fresh(1)[symmetric])
+apply(simp add: Abs1_eq_iff_fresh(1)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
-apply(subst Abs1_eq_fresh(1))
+apply(subst Abs1_eq_iff_fresh(1))
 apply(auto simp add: fresh_Pair)[1]
 apply(assumption)
-apply(simp add: Abs1_eq_fresh(2)[symmetric])
+apply(simp add: Abs1_eq_iff_fresh(2)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
-apply(subst Abs1_eq_fresh(2))
+apply(subst Abs1_eq_iff_fresh(2))
 apply(auto simp add: fresh_Pair)[1]
 apply(assumption)
-apply(simp add: Abs1_eq_fresh(3)[symmetric])
+apply(simp add: Abs1_eq_iff_fresh(3)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
-apply(subst Abs1_eq_fresh(3))
+apply(subst Abs1_eq_iff_fresh(3))
 apply(auto simp add: fresh_Pair)[1]
 apply(assumption)
 done
@@ -964,6 +964,35 @@
 using assms by (auto simp add: Abs1_eq_iff fresh_permute_left)
 
 
+ML {*
+fun alpha_single_simproc thm _ ss ctrm =
+ let
+    val ctxt = Simplifier.the_context ss
+    val thy = Proof_Context.theory_of ctxt
+    val _ $ (_ $ x) $ (_ $ y) = term_of ctrm
+    val cvrs = union (op =) (Term.add_frees x []) (Term.add_frees y [])
+      |> filter (fn (_, ty) => Sign.of_sort thy (ty, @{sort fs}))
+      |> map Free
+      |> HOLogic.mk_tuple
+      |> Thm.cterm_of thy
+    val cvrs_ty = ctyp_of_term cvrs
+    val thm' = thm
+      |> Drule.instantiate' [NONE, NONE, SOME cvrs_ty] [NONE, NONE, NONE, NONE, SOME cvrs] 
+  in
+    SOME thm'
+  end
+*}
+
+simproc_setup alpha_set ("[{atom a}]set. x = [{atom b}]set. y") = 
+  {* alpha_single_simproc @{thm Abs1_eq_iff_all(1)[THEN eq_reflection]} *}
+
+simproc_setup alpha_res ("[{atom a}]res. x = [{atom b}]res. y") = 
+  {* alpha_single_simproc @{thm Abs1_eq_iff_all(2)[THEN eq_reflection]} *}
+
+simproc_setup alpha_lst ("[[atom a]]lst. x = [[atom b]]lst. y") = 
+  {* alpha_single_simproc @{thm Abs1_eq_iff_all(3)[THEN eq_reflection]} *}
+
+
 subsection {* Renaming of bodies of abstractions *}
 
 lemma Abs_rename_set:

--- a/Tutorial/Lambda.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Tutorial/Lambda.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -41,6 +41,7 @@
 apply(simp add: eqvt_def height_graph_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
+using [[simproc del: alpha_lst]]
 apply(auto)
 apply(erule_tac c="()" in Abs_lst1_fcb2)
 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
@@ -61,6 +62,7 @@
   unfolding eqvt_def subst_graph_def
   apply(rule, perm_simp, rule)
   apply(rule TrueI)
+  using [[simproc del: alpha_lst]]
   apply(auto)
   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
   apply(blast)+

--- a/Tutorial/Tutorial2.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Tutorial/Tutorial2.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -376,7 +376,7 @@
   moreover 
   have "Lam [x]. Var x \<mapsto> Var x" using unbind_simple by auto
   ultimately 
-  have "atom x \<sharp> Var x" using unbind_fake by auto
+  have "atom x \<sharp> Var x" using unbind_fake by blast
   then have "x \<noteq> x" by (simp add: lam.fresh fresh_at_base)
   then show "False" by simp
 qed

--- a/Tutorial/Tutorial5.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Tutorial/Tutorial5.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -127,12 +127,13 @@
   obtains T1 T2 where "T = T1 \<rightarrow> T2" "(x, T1) # \<Gamma> \<turnstile> t : T2"
 using ty fc
 apply(cases)
+using [[simproc del: alpha_lst]]
 apply(auto simp add: lam.eq_iff lam.distinct ty.eq_iff)
 apply(auto simp add: Abs1_eq_iff)
 apply(rotate_tac 3)
 apply(drule_tac p="(x \<leftrightarrow> xa)" in permute_boolI)
 apply(perm_simp)
-apply(auto simp add: flip_def swap_fresh_fresh ty_fresh)
+apply(auto simp add: flip_fresh_fresh ty_fresh)
 done