diff -r 636de31888a6 -r fcc660ece040 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Wed Apr 14 16:05:58 2010 +0200
+++ b/Nominal/Abs.thy	Wed Apr 14 18:46:59 2010 +0200
@@ -762,8 +762,7 @@
   by (simp_all add: fresh_plus_perm)
 
 
-(* PROBLEM: this should be the real eqvt lemma for the alphas *)
-lemma alpha_gen_real_eqvt:
+lemma alpha_gen_eqvt[eqvt]:
   shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
   and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
   and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
@@ -774,23 +773,6 @@
   unfolding Diff_eqvt[symmetric]
   by (auto simp add: permute_bool_def fresh_star_permute_iff)
 
-
-lemma alpha_gen_eqvt:
-  assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
-  and     b: "p \<bullet> (f x) = f (p \<bullet> x)"
-  and     c: "p \<bullet> (f y) = f (p \<bullet> y)"
-  shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
-  and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
-  and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst R f (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
-  unfolding alphas
-  unfolding set_eqvt[symmetric]
-  unfolding b[symmetric] c[symmetric]
-  unfolding Diff_eqvt[symmetric]
-  unfolding permute_eqvt[symmetric]
-  using a
-  by (auto simp add: fresh_star_permute_iff)
-
-
 lemma alpha_gen_simpler:
   assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
   and fin_fv: "finite (f x)"